srings_3.miz

    begin

    theorem :: SRINGS_3:1



     Lem10: for f1,f2 be FinSequence, k be Nat st k in ( Seg (( len f1) * ( len f2))) holds (((k -' 1) mod ( len f2)) + 1) in ( dom f2) & (((k -' 1) div ( len f2)) + 1) in ( dom f1)

    proof

      let f1,f2 be FinSequence;

      let k be Nat;

      reconsider i1 = (((k -' 1) div ( len f2)) + 1) as Nat;

      reconsider i2 = (((k -' 1) mod ( len f2)) + 1) as Nat;

      assume

       B1: k in ( Seg (( len f1) * ( len f2)));

      then

       B2: 1 <= k & k <= (( len f1) * ( len f2)) by FINSEQ_1: 1;

      then

       B3: 1 <= (( len f1) * ( len f2)) by XXREAL_0: 2;



       B4: ( len f1) <> 0 & ( len f2) <> 0 by B1;

      then (((k -' 1) mod ( len f2)) + 1) <= ( len f2) by NAT_1: 13, NAT_D: 1;

      hence (((k -' 1) mod ( len f2)) + 1) in ( dom f2) by NAT_1: 11, FINSEQ_3: 25;

      1 <= ( len f1) & 1 <= ( len f2) by B4, NAT_1: 14;



      then

       B6: (((( len f1) * ( len f2)) -' 1) div ( len f2)) = (((( len f1) * ( len f2)) div ( len f2)) - 1) by B3, NAT_2: 15, NAT_D:def 3

      .= (( len f1) - 1) by B4, NAT_D: 18;

      (k -' 1) <= ((( len f1) * ( len f2)) -' 1) by B2, NAT_D: 42;

      then ((k -' 1) div ( len f2)) <= (((( len f1) * ( len f2)) -' 1) div ( len f2)) by NAT_2: 24;

      then i1 <= ((( len f1) - 1) + 1) by B6, XREAL_1: 6;

      hence (((k -' 1) div ( len f2)) + 1) in ( dom f1) by NAT_1: 11, FINSEQ_3: 25;

    end;

    theorem :: SRINGS_3:2



     CANFS: for S be non empty finite set holds ( Union ( canFS S)) = ( union S)

    proof

      let S be non empty finite set;

      now

        let x be object;

        assume x in ( union S);

        then

        consider A be set such that

         A2: x in A & A in S by TARSKI:def 4;

        A in ( rng ( canFS S)) by A2, DIST_2: 3;

        hence x in ( union ( rng ( canFS S))) by A2, TARSKI:def 4;

      end;

      then ( union S) c= ( union ( rng ( canFS S)));

      hence thesis by ZFMISC_1: 77;

    end;

    theorem :: SRINGS_3:3



     TTT1: for x be object holds <*x*> is disjoint_valued FinSequence

    proof

      let x be object;

      now

        let i,j be object;

        assume

         A1: i <> j;



         A2: ( dom <*x*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

        per cases ;

          suppose i in ( dom <*x*>);

          then i = 1 by A2, TARSKI:def 1;

          then not j in {1} by A1, TARSKI:def 1;

          then ( <*x*> . j) = {} by A2, FUNCT_1:def 2;

          hence ( <*x*> . i) misses ( <*x*> . j);

        end;

          suppose not i in ( dom <*x*>);

          then ( <*x*> . i) = {} by FUNCT_1:def 2;

          hence ( <*x*> . i) misses ( <*x*> . j);

        end;

      end;

      hence thesis by PROB_2:def 2;

    end;

    theorem :: SRINGS_3:4



     Disjoint2: for x,y be set, F be FinSequence st F = <*x, y*> & x misses y holds F is disjoint_valued

    proof

      let x,y be set, F be FinSequence;

      assume

       A1: F = <*x, y*> & x misses y;

      now

        let i,j be object;

        assume

         A6: i <> j;

        per cases ;

          suppose not i in ( dom F) or not j in ( dom F);

          then (F . i) = {} or (F . j) = {} by FUNCT_1:def 2;

          hence (F . i) misses (F . j);

        end;

          suppose

           A7: i in ( dom F) & j in ( dom F);



           A8: ( len F) = 2 & (F . 1) = x & (F . 2) = y by A1, FINSEQ_1: 44;

          then i in {1, 2} & j in {1, 2} by A7, FINSEQ_1:def 3, FINSEQ_1: 2;

          then (i = 1 or i = 2) & (j = 1 or j = 2) by TARSKI:def 2;

          hence (F . i) misses (F . j) by A1, A6, A8;

        end;

      end;

      hence F is disjoint_valued by PROB_2:def 2;

    end;

    theorem :: SRINGS_3:5



     TT1: for f1,f2 be FinSequence holds ex f be FinSequence st (( Union f1) /\ ( Union f2)) = ( Union f) & ( dom f) = ( Seg (( len f1) * ( len f2))) & for i be Nat st i in ( dom f) holds (f . i) = ((f1 . (((i -' 1) div ( len f2)) + 1)) /\ (f2 . (((i -' 1) mod ( len f2)) + 1)))

    proof

      let f1,f2 be FinSequence;



       A0: for k be Nat st k in ( Seg (( len f1) * ( len f2))) holds (((k -' 1) mod ( len f2)) + 1) in ( dom f2) & (((k -' 1) div ( len f2)) + 1) in ( dom f1) by Lem10;

      defpred P[ Nat, object] means $2 = ((f1 . ((($1 -' 1) div ( len f2)) + 1)) /\ (f2 . ((($1 -' 1) mod ( len f2)) + 1)));



       A1: for k be Nat st k in ( Seg (( len f1) * ( len f2))) holds ex x be object st P[k, x];

      consider f be FinSequence such that

       A8: ( dom f) = ( Seg (( len f1) * ( len f2))) & for k be Nat st k in ( Seg (( len f1) * ( len f2))) holds P[k, (f . k)] from FINSEQ_1:sch 1( A1);

      take f;

      now

        let x be object;

        assume x in (( Union f1) /\ ( Union f2));

        then

         A9: x in ( union ( rng f1)) & x in ( union ( rng f2)) by XBOOLE_0:def 4;

        then

        consider F1 be set such that

         A10: x in F1 & F1 in ( rng f1) by TARSKI:def 4;

        consider F2 be set such that

         A11: x in F2 & F2 in ( rng f2) by A9, TARSKI:def 4;

        consider i be object such that

         A12: i in ( dom f1) & F1 = (f1 . i) by A10, FUNCT_1:def 3;

        reconsider i as Nat by A12;

        consider j be object such that

         A13: j in ( dom f2) & F2 = (f2 . j) by A11, FUNCT_1:def 3;

        reconsider j as Nat by A13;

        set k = ((( len f2) * (i -' 1)) + j);



         E4: 1 <= i & i <= ( len f1) & 1 <= j & j <= ( len f2) by A12, A13, FINSEQ_3: 25;

        then

         F5: 1 <= k by NAT_1: 12;

        (k -' 1) = (((( len f2) * (i -' 1)) + j) - 1) by E4, NAT_D: 37;

        then

         E5: (k -' 1) = ((( len f2) * (i -' 1)) + (j - 1));



         E7: (i - 1) = (i -' 1) & (j - 1) = (j -' 1) by E4, XREAL_1: 48, XREAL_0:def 2;

        then

         E8: ((k -' 1) div ( len f2)) = (((j -' 1) div ( len f2)) + (i -' 1)) by E4, E5, NAT_D: 61;

        (j -' 1) < j by E7, XREAL_1: 44;

        then

         F0: (j -' 1) < ( len f2) by E4, XXREAL_0: 2;

        then ((j -' 1) div ( len f2)) = 0 by NAT_D: 27;

        then

         F1: F1 = (f1 . (((k -' 1) div ( len f2)) + 1)) by A12, E7, E8;

        ((k -' 1) mod ( len f2)) = ((j -' 1) mod ( len f2)) by E5, E7, NAT_D: 61;

        then ((k -' 1) mod ( len f2)) = (j -' 1) by F0, NAT_D: 24;

        then

         F3: F2 = (f2 . (((k -' 1) mod ( len f2)) + 1)) by A13, E7;

        (i -' 1) <= (( len f1) - 1) by E4, E7, XREAL_1: 9;

        then ((i -' 1) * ( len f2)) <= ((( len f1) - 1) * ( len f2)) by XREAL_1: 66;

        then k <= (((( len f1) - 1) * ( len f2)) + ( len f2)) by E4, XREAL_1: 7;

        then

         F4: k in ( Seg (( len f1) * ( len f2))) by F5;

        then (f . k) = (F1 /\ F2) by A8, F1, F3;

        then x in (f . k) & (f . k) in ( rng f) by A10, A11, F4, A8, FUNCT_1: 3, XBOOLE_0:def 4;

        hence x in ( Union f) by TARSKI:def 4;

      end;

      then

       P1: (( Union f1) /\ ( Union f2)) c= ( Union f);

      now

        let x be object;

        assume x in ( Union f);

        then

        consider F be set such that

         G1: x in F & F in ( rng f) by TARSKI:def 4;

        consider i be object such that

         G2: i in ( dom f) & F = (f . i) by G1, FUNCT_1:def 3;

        reconsider i as Nat by G2;

        F = ((f1 . (((i -' 1) div ( len f2)) + 1)) /\ (f2 . (((i -' 1) mod ( len f2)) + 1))) by A8, G2;

        then

         G3: x in (f1 . (((i -' 1) div ( len f2)) + 1)) & x in (f2 . (((i -' 1) mod ( len f2)) + 1)) by G1, XBOOLE_0:def 4;

        (f1 . (((i -' 1) div ( len f2)) + 1)) in ( rng f1) & (f2 . (((i -' 1) mod ( len f2)) + 1)) in ( rng f2) by G2, A8, A0, FUNCT_1: 3;

        then x in ( union ( rng f1)) & x in ( union ( rng f2)) by G3, TARSKI:def 4;

        hence x in (( Union f1) /\ ( Union f2)) by XBOOLE_0:def 4;

      end;

      then ( Union f) c= (( Union f1) /\ ( Union f2));

      hence thesis by A8, P1;

    end;

    theorem :: SRINGS_3:6



     TT2: for f1,f2 be disjoint_valued FinSequence holds ex f be disjoint_valued FinSequence st (( Union f1) /\ ( Union f2)) = ( Union f) & ( dom f) = ( Seg (( len f1) * ( len f2))) & for i be Nat st i in ( dom f) holds (f . i) = ((f1 . (((i -' 1) div ( len f2)) + 1)) /\ (f2 . (((i -' 1) mod ( len f2)) + 1)))

    proof

      let f1,f2 be disjoint_valued FinSequence;

      consider f be FinSequence such that

       A1: (( Union f1) /\ ( Union f2)) = ( Union f) & ( dom f) = ( Seg (( len f1) * ( len f2))) & for i be Nat st i in ( dom f) holds (f . i) = ((f1 . (((i -' 1) div ( len f2)) + 1)) /\ (f2 . (((i -' 1) mod ( len f2)) + 1))) by TT1;

      now

        let i,j be object;

        assume

         A2: i <> j;

        per cases ;

          suppose

           A3: i in ( dom f) & j in ( dom f);

          then

          reconsider i1 = i, j1 = j as Nat;

          (f . i) = ((f1 . (((i1 -' 1) div ( len f2)) + 1)) /\ (f2 . (((i1 -' 1) mod ( len f2)) + 1))) & (f . j) = ((f1 . (((j1 -' 1) div ( len f2)) + 1)) /\ (f2 . (((j1 -' 1) mod ( len f2)) + 1))) by A1, A3;

          then

           B1: (f . i) c= (f1 . (((i1 -' 1) div ( len f2)) + 1)) & (f . j) c= (f1 . (((j1 -' 1) div ( len f2)) + 1)) & (f . i) c= (f2 . (((i1 -' 1) mod ( len f2)) + 1)) & (f . j) c= (f2 . (((j1 -' 1) mod ( len f2)) + 1)) by XBOOLE_1: 17;



           A5: 0 < ( len f1) & 0 < ( len f2) or 0 > ( len f1) & 0 > ( len f2) by A1, A3;

           A6:

          now

            assume

             A7: (((i1 -' 1) div ( len f2)) + 1) = (((j1 -' 1) div ( len f2)) + 1) & (((i1 -' 1) mod ( len f2)) + 1) = (((j1 -' 1) mod ( len f2)) + 1);

            (i1 -' 1) = ((( len f2) * ((j1 -' 1) div ( len f2))) + ((i1 -' 1) mod ( len f2))) by A7, A5, NAT_D: 2

            .= (j1 -' 1) by A5, A7, NAT_D: 2;

            then (1 > i1 or i1 >= j1) & (1 > j1 or j1 >= i1) by NAT_D: 56;

            hence contradiction by A2, A1, A3, FINSEQ_1: 1, XXREAL_0: 1;

          end;

          per cases by A6;

            suppose (((i1 -' 1) div ( len f2)) + 1) <> (((j1 -' 1) div ( len f2)) + 1);

            hence (f . i) misses (f . j) by B1, XBOOLE_1: 64, PROB_2:def 2;

          end;

            suppose (((i1 -' 1) mod ( len f2)) + 1) <> (((j1 -' 1) mod ( len f2)) + 1);

            hence (f . i) misses (f . j) by B1, XBOOLE_1: 64, PROB_2:def 2;

          end;

        end;

          suppose not (i in ( dom f) & j in ( dom f));

          then (f . i) = {} or (f . j) = {} by FUNCT_1:def 2;

          hence (f . i) misses (f . j);

        end;

      end;

      then

      reconsider f as disjoint_valued FinSequence by PROB_2:def 2;

      take f;

      thus thesis by A1;

    end;

    theorem :: SRINGS_3:7



     NE: for X be set, S be non empty diff-closed Subset-Family of X holds {} in S

    proof

      let X be set, S be non empty diff-closed Subset-Family of X;

      consider A be object such that

       A1: A in S by XBOOLE_0:def 1;

      reconsider A as set by TARSKI: 1;

      (A \ A) in S by A1, FINSUB_1:def 3;

      hence {} in S by XBOOLE_1: 37;

    end;

    registration

      let X be set;

      cluster non empty diff-closed -> with_empty_element for Subset-Family of X;

      coherence

      proof

        let S be Subset-Family of X;

        assume

         A0: S is non empty diff-closed;

        then

        consider A be object such that

         A1: A in S;

        reconsider A as set by TARSKI: 1;

        (A \ A) in S by A0, A1;

        hence thesis by XBOOLE_1: 37;

      end;

    end

    begin

    definition

      let IT be set;

      :: SRINGS_3:def1

      attr IT is semi-diff-closed means

      : DefSD: for X,Y be set st X in IT & Y in IT holds ex F be disjoint_valued FinSequence of IT st (X \ Y) = ( Union F);

    end



     TV1: for X be set holds ( bool X) is semi-diff-closed

    proof

      let X be set;

      set S = ( bool X);

      thus S is semi-diff-closed

      proof

        let A,B be set;

        assume A in S & B in S;

        then (A \ B) c= X by XBOOLE_1: 1;

        then {(A \ B)} c= S by ZFMISC_1: 31;

        then ( rng <*(A \ B)*>) c= S by FINSEQ_1: 38;

        then

        reconsider F = <*(A \ B)*> as FinSequence of S by FINSEQ_1:def 4;

        now

          let i,j be object;

          assume

           A1: i <> j;

           A2:

          now

            assume i in ( dom F) & j in ( dom F);

            then i in {1} & j in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

            then i = 1 & j = 1 by TARSKI:def 1;

            hence contradiction by A1;

          end;

          per cases by A2;

            suppose not i in ( dom F);

            then (F . i) = {} by FUNCT_1:def 2;

            hence (F . i) misses (F . j);

          end;

            suppose not j in ( dom F);

            then (F . j) = {} by FUNCT_1:def 2;

            hence (F . i) misses (F . j);

          end;

        end;

        then

        reconsider F as disjoint_valued FinSequence of S by PROB_2:def 2;

        take F;

        ( union ( rng F)) = ( union {(A \ B)}) by FINSEQ_1: 38;

        hence (A \ B) = ( Union F);

      end;

    end;

    registration

      let X be set;

      cluster ( bool X) -> semi-diff-closed;

      coherence by TV1;

    end

    registration

      let X be set;

      cluster non empty semi-diff-closed cap-closed for Subset-Family of X;

      existence

      proof

        reconsider S = ( bool X) as Subset-Family of X;

        take S;

        thus thesis;

      end;

    end

    registration

      let X be set;

      cluster with_empty_element semi-diff-closed cap-closed for Subset-Family of X;

      existence

      proof

        ( bool X) is non empty semi-diff-closed cap-closed Subset-Family of X;

        hence thesis;

      end;

    end

    definition

      let X be set;

      mode Semiring of X is with_empty_element semi-diff-closed cap-closed Subset-Family of X;

    end

    theorem :: SRINGS_3:8



     Lm1: for X be set, S be Subset-Family of X, S1,S2 be set st S1 in S & S2 in S & S is semi-diff-closed holds ex x be finite Subset of S st x is a_partition of (S1 \ S2)

    proof

      let X be set, S be Subset-Family of X, S1,S2 be set;

      assume S1 in S & S2 in S & S is semi-diff-closed;

      then

      consider F be disjoint_valued FinSequence of S such that

       Y2: (S1 \ S2) = ( Union F);

      reconsider x = (( rng F) \ { {} }) as finite Subset of S;

      take x;

      now

        let p be object;

        assume

         U1: p in x;

        then p in S;

        then

        reconsider p1 = p as Subset of X;

        p in ( rng F) & not p in { {} } by U1, XBOOLE_0:def 5;

        then p1 c= (S1 \ S2) by Y2, TARSKI:def 4;

        hence p in ( bool (S1 \ S2));

      end;

      then

       Y5: x c= ( bool (S1 \ S2));



       Y3: ( union x) = (S1 \ S2) by Y2, PARTIT1: 2;

      now

        let A be Subset of (S1 \ S2);

        assume A in x;

        then

         Y6: A in ( rng F) & not A in { {} } by XBOOLE_0:def 5;

        hence A <> {} by TARSKI:def 1;

        now

          let B be Subset of (S1 \ S2);

          assume B in x;

          then B in ( rng F) & not B in { {} } by XBOOLE_0:def 5;

          then (ex i be Nat st i in ( dom F) & (F . i) = A) & (ex j be Nat st j in ( dom F) & (F . j) = B) by Y6, FINSEQ_2: 10;

          hence A = B or A misses B by PROB_2:def 2;

        end;

        hence for B be Subset of (S1 \ S2) st B in x holds A = B or A misses B;

      end;

      hence x is a_partition of (S1 \ S2) by Y3, Y5, EQREL_1:def 4;

    end;

    theorem :: SRINGS_3:9

    for X be set, S be non empty Subset-Family of X st S is semi-diff-closed holds S is diff-c=-finite-partition-closed

    proof

      let X be set, S be non empty Subset-Family of X;

      assume S is semi-diff-closed;

      then for S1,S2 be Element of S st S2 c= S1 holds ex x be finite Subset of S st x is a_partition of (S1 \ S2) by Lm1;

      hence S is diff-c=-finite-partition-closed by SRINGS_1:def 3;

    end;

    theorem :: SRINGS_3:10



     th10: for X be set, S be Subset-Family of X st S is with_empty_element & S is cap-finite-partition-closed & S is diff-c=-finite-partition-closed holds S is semi-diff-closed

    proof

      let X be set, S be Subset-Family of X;

      assume that

       A0: S is with_empty_element and

       A1: S is cap-finite-partition-closed and

       A2: S is diff-c=-finite-partition-closed;

      now

        let S1,S2 be set;

        assume

         A3: S1 in S & S2 in S;

        per cases ;

          suppose

           X1: (S1 \ S2) <> {} ;

          then

          consider x be finite Subset of S such that

           L4: x is a_partition of (S1 \ S2) by A1, A2, A3, SRINGS_1:def 2;



           L8: ( union x) = (S1 \ S2) & for A be Subset of (S1 \ S2) st A in x holds A <> {} & for B be Subset of (S1 \ S2) st B in x holds A = B or A misses B by L4, EQREL_1:def 4;



           L5: ( rng ( canFS x)) c= x;

          ( rng ( canFS x)) c= S by XBOOLE_1: 1;

          then

          reconsider F = ( canFS x) as FinSequence of S by FINSEQ_1:def 4;

          now

            let i,j be object;

            assume

             L6: i <> j;

            per cases ;

              suppose

               L10: i in ( dom F) & j in ( dom F);

              then (F . i) in x & (F . j) in x by L5, FUNCT_1: 3;

              then (F . i) = (F . j) or (F . i) misses (F . j) by L4, EQREL_1:def 4;

              hence (F . i) misses (F . j) by L6, L10, FUNCT_1:def 4;

            end;

              suppose not i in ( dom F) or not j in ( dom F);

              then (F . i) = {} or (F . j) = {} by FUNCT_1:def 2;

              hence (F . i) misses (F . j);

            end;

          end;

          then

          reconsider F as disjoint_valued FinSequence of S by PROB_2:def 2;

          take F;

          thus ( Union F) = (S1 \ S2) by L4, X1, L8, CANFS;

        end;

          suppose

           T0: (S1 \ S2) = {} ;

          set F = ( canFS { {} });

           { {} } c= S by A0, SETFAM_1:def 8, ZFMISC_1: 31;

          then ( rng F) c= S;

          then

          reconsider F as FinSequence of S by FINSEQ_1:def 4;



           T3: F = <* {} *> by FINSEQ_1: 94;

          now

            let i,j be object;

            assume i <> j;

            i in ( dom F) implies i = 1 by T3, FINSEQ_1: 90;

            then (F . i) = {} by T3, FINSEQ_1: 40, FUNCT_1:def 2;

            hence (F . i) misses (F . j);

          end;

          then

          reconsider F as disjoint_valued FinSequence of S by PROB_2:def 2;

          take F;

          ( Union F) = ( union { {} }) by CANFS;

          hence (S1 \ S2) = ( Union F) by T0;

        end;

      end;

      hence S is semi-diff-closed;

    end;

    registration

      cluster diff-closed -> semi-diff-closed cap-closed for set;

      correctness

      proof

        let R be set;

        assume

         A1: R is diff-closed;

        now

          let A,B be set;

          assume A in R & B in R;

          then (A \ B) in R by A1;

          then

          reconsider F = <*(A \ B)*> as FinSequence of R by FINSEQ_1: 74;

          now

            let x,y be object;

            assume

             A3: x <> y;



             A4: ( dom F) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

            per cases ;

              suppose x in ( dom F);

              then x = 1 by A4, TARSKI:def 1;

              then not y in ( dom F) by A3, A4, TARSKI:def 1;

              then (F . y) = {} by FUNCT_1:def 2;

              hence (F . x) misses (F . y);

            end;

              suppose not x in ( dom F);

              then (F . x) = {} by FUNCT_1:def 2;

              hence (F . x) misses (F . y);

            end;

          end;

          then

           A5: F is disjoint_valued by PROB_2:def 2;

          ( rng F) = {(A \ B)} by FINSEQ_1: 38;

          then ( Union F) = (A \ B);

          hence ex F be disjoint_valued FinSequence of R st (A \ B) = ( Union F) by A5;

        end;

        hence R is semi-diff-closed;

        now

          let A,B be set;

          assume

           A6: A in R & B in R;

          then (A \ B) in R by A1;

          then (A \ (A \ B)) in R by A1, A6;

          hence (A /\ B) in R by XBOOLE_1: 48;

        end;

        hence R is cap-closed;

      end;

    end

    registration

      let X be set;

      cluster non empty preBoolean for Subset-Family of X;

      existence

      proof

        ( bool X) is non empty preBoolean;

        hence thesis;

      end;

    end

    registration

      cluster non empty preBoolean -> with_empty_element for set;

      correctness

      proof

        let X be set;

        assume

         A1: X is non empty preBoolean;

        then

        consider x be object such that

         A2: x in X;

        reconsider x1 = x as set by A2;

         {} = (x1 \ x1) by XBOOLE_1: 37;

        then {} in X by A1, A2, FINSUB_1:def 3;

        hence X is with_empty_element;

      end;

    end



     ExistRing: for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X holds ex Y be non empty preBoolean Subset-Family of X st Y = ( meet { Z where Z be non empty preBoolean Subset-Family of X : S c= Z })

    proof

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X;

      set V = { Z where Z be non empty preBoolean Subset-Family of X : S c= Z };



       A1: ( bool X) in V;

      then

      reconsider Y = ( meet V) as Subset-Family of X by SETFAM_1: 3;

      now

        let Z be set;

        assume Z in V;

        then ex S1 be non empty preBoolean Subset-Family of X st Z = S1 & S c= S1;

        hence {} in Z by SETFAM_1:def 8;

      end;

      then

       A2: Y is non empty by A1, SETFAM_1:def 1;

      now

        let A,B be set;

        assume

         B1: A in Y & B in Y;

        for Z be set st Z in V holds (A \/ B) in Z

        proof

          let Z be set;

          assume

           B2: Z in V;

          then

          consider Z1 be non empty preBoolean Subset-Family of X such that

           B3: Z = Z1 & S c= Z1;

          A in Z1 & B in Z1 by B1, B2, B3, SETFAM_1:def 1;

          hence (A \/ B) in Z by B3, FINSUB_1:def 1;

        end;

        hence (A \/ B) in Y by A1, SETFAM_1:def 1;

      end;

      then

       B4: Y is cup-closed;

      now

        let A,B be set;

        assume

         C1: A in Y & B in Y;

        for Z be set st Z in V holds (A \ B) in Z

        proof

          let Z be set;

          assume

           C2: Z in V;

          then

          consider Z1 be non empty preBoolean Subset-Family of X such that

           C3: Z = Z1 & S c= Z1;

          A in Z1 & B in Z1 by C1, C2, C3, SETFAM_1:def 1;

          hence (A \ B) in Z by C3, FINSUB_1:def 3;

        end;

        hence (A \ B) in Y by A1, SETFAM_1:def 1;

      end;

      then Y is diff-closed;

      hence thesis by A2, B4;

    end;

    definition

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X;

      :: SRINGS_3:def2

      func Ring_generated_by S -> non empty preBoolean Subset-Family of X equals ( meet { Z where Z be non empty preBoolean Subset-Family of X : S c= Z });

      correctness

      proof

        consider Y be non empty preBoolean Subset-Family of X such that

         A1: Y = ( meet { Z where Z be non empty preBoolean Subset-Family of X : S c= Z }) by ExistRing;

        thus thesis by A1;

      end;

    end

    theorem :: SRINGS_3:11



     RingGen1: for X be set, P be with_empty_element semi-diff-closed cap-closed Subset-Family of X holds P c= ( Ring_generated_by P)

    proof

      let X be set, P be with_empty_element semi-diff-closed cap-closed Subset-Family of X;

      set Y = { Z where Z be non empty preBoolean Subset-Family of X : P c= Z };



       A1: ( bool X) in Y;

      for A be set st A in Y holds P c= A

      proof

        let A be set;

        assume A in Y;

        then ex Z be non empty preBoolean Subset-Family of X st A = Z & P c= Z;

        hence P c= A;

      end;

      hence thesis by A1, SETFAM_1: 5;

    end;



     lemma100: for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be set st P = { A where A be Subset of X : ex F be disjoint_valued FinSequence of S st A = ( Union F) } holds P is non empty Subset-Family of X & S c= P

    proof

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be set;

      assume

       A1: P = { A where A be Subset of X : ex F be disjoint_valued FinSequence of S st A = ( Union F) };

      reconsider E0 = {} as Subset of X by XBOOLE_1: 2;

      reconsider g0 = <*E0*> as disjoint_valued FinSequence by TTT1;

      now

        let i be Nat;

        assume i in ( dom g0);

        then i in ( Seg 1) by FINSEQ_1: 38;

        then i = 1 by TARSKI:def 1, FINSEQ_1: 2;

        then (g0 . i) = E0 by FINSEQ_1: 40;

        hence (g0 . i) in S by SETFAM_1:def 8;

      end;

      then

      reconsider g0 as disjoint_valued FinSequence of S by FINSEQ_2: 12;

      ( Union g0) = ( union {E0}) by FINSEQ_1: 38;

      then

       A5: {} in P by A1;

      now

        let x be object;

        assume x in P;

        then ex A be Subset of X st x = A & ex F be disjoint_valued FinSequence of S st A = ( Union F) by A1;

        hence x in ( bool X);

      end;

      hence P is non empty Subset-Family of X by A5, TARSKI:def 3;

      now

        let x be object;

        assume

         A5: x in S;

        then

        reconsider x1 = x as Subset of X;

        set g = <*x1*>;



         A3: ( rng <*x1*>) = {x1} by FINSEQ_1: 38;

        reconsider g as disjoint_valued FinSequence by TTT1;

        now

          let y be object;

          assume y in ( rng g);

          then

          consider i be object such that

           B1: i in ( dom g) & y = (g . i) by FUNCT_1:def 3;

          reconsider i as Element of NAT by B1;

          i in ( Seg 1) by B1, FINSEQ_1: 38;

          then i = 1 by TARSKI:def 1, FINSEQ_1: 2;

          hence y in S by B1, A5, FINSEQ_1: 40;

        end;

        then ( rng g) c= S;

        then

        reconsider g as disjoint_valued FinSequence of S by FINSEQ_1:def 4;

        ( Union g) = x by A3;

        hence x in P by A1;

      end;

      hence S c= P;

    end;

    definition

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X;

      :: SRINGS_3:def3

      func DisUnion S -> non empty Subset-Family of X equals { A where A be Subset of X : ex F be disjoint_valued FinSequence of S st A = ( Union F) };

      coherence by lemma100;

    end

    theorem :: SRINGS_3:12

    for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X holds S c= ( DisUnion S) by lemma100;

    theorem :: SRINGS_3:13



     lemma101: for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X holds ( DisUnion S) is cap-closed

    proof

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X;

      set P = ( DisUnion S);

      now

        let x,y be set;

        assume

         C1: x in P & y in P;

        then

        consider x1 be Subset of X such that

         C2: x = x1 & ex g be disjoint_valued FinSequence of S st x1 = ( Union g);

        consider g1 be disjoint_valued FinSequence of S such that

         C3: x1 = ( Union g1) by C2;

        consider y1 be Subset of X such that

         C4: y = y1 & ex g be disjoint_valued FinSequence of S st y1 = ( Union g) by C1;

        consider g2 be disjoint_valued FinSequence of S such that

         C5: y1 = ( Union g2) by C4;

        consider h be disjoint_valued FinSequence such that

         C6: (( Union g1) /\ ( Union g2)) = ( Union h) & ( dom h) = ( Seg (( len g1) * ( len g2))) & for i be Nat st i in ( dom h) holds (h . i) = ((g1 . (((i -' 1) div ( len g2)) + 1)) /\ (g2 . (((i -' 1) mod ( len g2)) + 1))) by TT2;

        (x1 /\ y1) c= X;

        then

        reconsider xy = (x /\ y) as Subset of X by C2, C4;

        now

          let i be Nat;

          assume

           C9: i in ( dom h);

          then (((i -' 1) mod ( len g2)) + 1) in ( dom g2) & (((i -' 1) div ( len g2)) + 1) in ( dom g1) by C6, Lem10;

          then (g1 . (((i -' 1) div ( len g2)) + 1)) in S & (g2 . (((i -' 1) mod ( len g2)) + 1)) in S by FINSEQ_2: 11;

          then ((g1 . (((i -' 1) div ( len g2)) + 1)) /\ (g2 . (((i -' 1) mod ( len g2)) + 1))) in S by FINSUB_1:def 2;

          hence (h . i) in S by C9, C6;

        end;

        then

        reconsider h as disjoint_valued FinSequence of S by FINSEQ_2: 12;

        xy = ( Union h) by C2, C4, C3, C5, C6;

        hence (x /\ y) in P;

      end;

      hence P is cap-closed;

    end;

    theorem :: SRINGS_3:14



     lemma102: for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, A,B,P be set st P = ( DisUnion S) & A in P & B in P & A misses B holds (A \/ B) in P

    proof

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, A,B,P be set;

      assume that

       A1: P = ( DisUnion S) and

       A2: A in P & B in P & A misses B;

      consider A1 be Subset of X such that

       A3: A = A1 & ex g be disjoint_valued FinSequence of S st A1 = ( Union g) by A1, A2;

      consider g1 be disjoint_valued FinSequence of S such that

       A4: A1 = ( Union g1) by A3;

      consider B1 be Subset of X such that

       A5: B = B1 & ex g be disjoint_valued FinSequence of S st B1 = ( Union g) by A1, A2;

      consider g2 be disjoint_valued FinSequence of S such that

       A6: B1 = ( Union g2) by A5;

      set F = (g1 ^ g2);

      now

        let n,m be object;

        assume

         A7: n <> m;

        per cases ;

          suppose

           A8: n in ( dom F) & m in ( dom F);

          then

          reconsider n1 = n, m1 = m as Nat;



           A9: n1 in ( dom g1) or ex k be Nat st k in ( dom g2) & n1 = (( len g1) + k) by A8, FINSEQ_1: 25;



           A10: m1 in ( dom g1) or ex k be Nat st k in ( dom g2) & m1 = (( len g1) + k) by A8, FINSEQ_1: 25;

          per cases by A9, A10;

            suppose n1 in ( dom g1) & m1 in ( dom g1);

            then (F . n) = (g1 . n1) & (F . m) = (g1 . m1) by FINSEQ_1:def 7;

            hence (F . n) misses (F . m) by A7, PROB_2:def 2;

          end;

            suppose

             A11: n1 in ( dom g1) & ex k be Nat st k in ( dom g2) & m1 = (( len g1) + k);

            then

            consider k be Nat such that

             A12: k in ( dom g2) & m1 = (( len g1) + k);

            (F . n) = (g1 . n1) & (F . m) = (g2 . k) by A11, A12, FINSEQ_1:def 7;

            then

             A13: (F . n) in ( rng g1) & (F . m) in ( rng g2) by A11, A12, FUNCT_1: 3;

            now

              assume (F . n) meets (F . m);

              then

              consider x be object such that

               A14: x in (F . n) & x in (F . m) by XBOOLE_0: 3;

              x in ( union ( rng g1)) & x in ( union ( rng g2)) by A13, A14, TARSKI:def 4;

              hence contradiction by A2, A3, A5, A4, A6, XBOOLE_0:def 4;

            end;

            hence (F . n) misses (F . m);

          end;

            suppose

             A15: m1 in ( dom g1) & ex k be Nat st k in ( dom g2) & n1 = (( len g1) + k);

            then

            consider k be Nat such that

             A16: k in ( dom g2) & n1 = (( len g1) + k);

            (F . n) = (g2 . k) & (F . m) = (g1 . m) by A15, A16, FINSEQ_1:def 7;

            then

             A17: (F . n) in ( rng g2) & (F . m) in ( rng g1) by A15, A16, FUNCT_1: 3;

            now

              assume (F . n) meets (F . m);

              then

              consider x be object such that

               A18: x in (F . n) & x in (F . m) by XBOOLE_0: 3;

              x in ( union ( rng g1)) & x in ( union ( rng g2)) by A17, A18, TARSKI:def 4;

              hence contradiction by A2, A3, A5, A4, A6, XBOOLE_0:def 4;

            end;

            hence (F . n) misses (F . m);

          end;

            suppose

             A19: ex k be Nat st k in ( dom g2) & n1 = (( len g1) + k) & ex k be Nat st k in ( dom g2) & m1 = (( len g1) + k);

            then

            consider k1 be Nat such that

             A20: k1 in ( dom g2) & n1 = (( len g1) + k1);

            consider k2 be Nat such that

             A21: k2 in ( dom g2) & m1 = (( len g1) + k2) by A19;

            (F . n) = (g2 . k1) & (F . m) = (g2 . k2) by A20, A21, FINSEQ_1:def 7;

            hence (F . n) misses (F . m) by A7, A20, A21, PROB_2:def 2;

          end;

        end;

          suppose not n in ( dom F) or not m in ( dom F);

          then (F . n) = {} or (F . m) = {} by FUNCT_1:def 2;

          hence (F . n) misses (F . m);

        end;

      end;

      then

      reconsider F as disjoint_valued FinSequence of S by PROB_2:def 2;

      ( rng F) = (( rng g1) \/ ( rng g2)) by FINSEQ_1: 31;

      then ( Union F) = (A1 \/ B1) by A4, A6, ZFMISC_1: 78;

      hence (A \/ B) in P by A1, A3, A5;

    end;

    theorem :: SRINGS_3:15



     lemma103: for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, A,B be set st A in S & B in S holds (B \ A) in ( DisUnion S)

    proof

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, A,B be set;

      assume

       A2: A in S & B in S;

      reconsider A1 = A, B1 = B as Subset of X by A2;

      ex F be disjoint_valued FinSequence of S st (B \ A) = ( Union F) by A2, DefSD;

      then (B1 \ A1) in ( DisUnion S);

      hence thesis;

    end;

    theorem :: SRINGS_3:16



     lemma104: for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, A,B be set st A in S & B in ( DisUnion S) holds (B \ A) in ( DisUnion S)

    proof

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, A,B be set;

      assume that

       A2: A in S & B in ( DisUnion S);

      reconsider A1 = A as Subset of X by A2;

      consider B1 be Subset of X such that

       A5: B = B1 & ex F be disjoint_valued FinSequence of S st B1 = ( Union F) by A2;

      consider g1 be disjoint_valued FinSequence of S such that

       A6: B1 = ( Union g1) by A5;

      reconsider R1 = ( DisUnion S) as non empty set;

      defpred P[ Nat, object] means $2 = ((g1 . $1) \ A1);



       A7: for k be Nat st k in ( Seg ( len g1)) holds ex x be Element of R1 st P[k, x]

      proof

        let k be Nat;

        assume k in ( Seg ( len g1));

        then k in ( dom g1) by FINSEQ_1:def 3;

        then (g1 . k) in ( rng g1) & ( rng g1) c= S by FUNCT_1: 3;

        then ((g1 . k) \ A1) in ( DisUnion S) by A2, lemma103;

        hence ex x be Element of R1 st P[k, x];

      end;

      consider g2 be FinSequence of R1 such that

       A8: ( dom g2) = ( Seg ( len g1)) & for k be Nat st k in ( Seg ( len g1)) holds P[k, (g2 . k)] from FINSEQ_1:sch 5( A7);



       A11: for n,m be Nat st n in ( dom g2) & m in ( dom g2) & n <> m holds (g2 . n) misses (g2 . m)

      proof

        let n,m be Nat;

        assume

         A9: n in ( dom g2) & m in ( dom g2) & n <> m;

        then

         A10: (g2 . n) = ((g1 . n) \ A1) & (g2 . m) = ((g1 . m) \ A1) by A8;

        (g1 . n) misses (g2 . m) by A10, A9, PROB_2:def 2, XBOOLE_1: 80;

        hence (g2 . n) misses (g2 . m) by A10, XBOOLE_1: 80;

      end;

      set R = ( DisUnion S);

      defpred P2[ Nat] means ( union ( rng (g2 | $1))) in R;

      ( union ( rng (g2 | 0 ))) in S & S c= R by lemma100, SETFAM_1:def 8, ZFMISC_1: 2;

      then

       A12: P2[ 0 ];



       A13: for k be Nat st P2[k] holds P2[(k + 1)]

      proof

        let k be Nat;

        assume

         A14: P2[k];

        per cases ;

          suppose

           A15: (k + 1) <= ( len g2);

          then

           A20: k <= ( len g2) & k <= (k + 1) by NAT_1: 13;

          then ( len (g2 | (k + 1))) = (k + 1) & (g2 | k) = ((g2 | (k + 1)) | k) by A15, FINSEQ_1: 59, FINSEQ_1: 82;

          then (g2 | (k + 1)) = ((g2 | k) ^ <*((g2 | (k + 1)) . (k + 1))*>) by FINSEQ_3: 55;



          then ( rng (g2 | (k + 1))) = (( rng (g2 | k)) \/ ( rng <*((g2 | (k + 1)) . (k + 1))*>)) by FINSEQ_1: 31

          .= (( rng (g2 | k)) \/ {((g2 | (k + 1)) . (k + 1))}) by FINSEQ_1: 38

          .= (( rng (g2 | k)) \/ {(g2 . (k + 1))}) by FINSEQ_3: 112;



          then

           A16: ( union ( rng (g2 | (k + 1)))) = (( union ( rng (g2 | k))) \/ ( union {(g2 . (k + 1))})) by ZFMISC_1: 78

          .= (( union ( rng (g2 | k))) \/ (g2 . (k + 1)));



           A24: (k + 1) in ( dom g2) by A15, FINSEQ_3: 25, NAT_1: 11;

           A25:

          now

            assume ( union ( rng (g2 | k))) meets (g2 . (k + 1));

            then

            consider x be object such that

             A17: x in ( union ( rng (g2 | k))) & x in (g2 . (k + 1)) by XBOOLE_0: 3;

            consider Z be set such that

             A18: x in Z & Z in ( rng (g2 | k)) by A17, TARSKI:def 4;

            consider i be object such that

             A19: i in ( dom (g2 | k)) & Z = ((g2 | k) . i) by A18, FUNCT_1:def 3;

            reconsider i as Nat by A19;

            i <= ( len (g2 | k)) by A19, FINSEQ_3: 25;

            then

             A21: i <= k by A20, FINSEQ_1: 59;

            then

             A22: Z = (g2 . i) by A19, FINSEQ_3: 112;



             A23: ( dom (g2 | k)) c= ( dom g2) by RELAT_1: 60;

            i <> (k + 1) by A21, NAT_1: 13;

            then Z misses (g2 . (k + 1)) by A11, A22, A23, A19, A24;

            hence contradiction by A17, A18, XBOOLE_0:def 4;

          end;

          (g2 . (k + 1)) in ( rng g2) & ( rng g2) c= R by A24, FUNCT_1: 3;

          hence ( union ( rng (g2 | (k + 1)))) in R by A14, A16, A25, lemma102;

        end;

          suppose (k + 1) > ( len g2);

          then (g2 | (k + 1)) = g2 & (g2 | k) = g2 by FINSEQ_1: 58, NAT_1: 13;

          hence ( union ( rng (g2 | (k + 1)))) in R by A14;

        end;

      end;

      for k be Nat holds P2[k] from NAT_1:sch 2( A12, A13);

      then

       C1: P2[( len g2)];

      now

        let x be object;

        assume x in ( union ( rng g2));

        then

        consider y be set such that

         B1: x in y & y in ( rng g2) by TARSKI:def 4;

        consider k be object such that

         B2: k in ( dom g2) & y = (g2 . k) by B1, FUNCT_1:def 3;

        reconsider k as Nat by B2;



         C3: (g2 . k) = ((g1 . k) \ A1) by B2, A8;

        then

         B3: x in (g1 . k) & not x in A1 by B1, B2, XBOOLE_0:def 5;

        k in ( dom g1) by B2, A8, FINSEQ_1:def 3;

        then (g1 . k) in ( rng g1) by FUNCT_1: 3;

        then x in ( union ( rng g1)) by C3, B1, B2, TARSKI:def 4;

        hence x in (( union ( rng g1)) \ A1) by B3, XBOOLE_0:def 5;

      end;

      then

       B4: ( union ( rng g2)) c= (( union ( rng g1)) \ A1);

      now

        let x be object;

        assume

         C5: x in (( union ( rng g1)) \ A1);

        then

         B5: x in ( union ( rng g1)) & not x in A1 by XBOOLE_0:def 5;

        consider y be set such that

         B6: x in y & y in ( rng g1) by C5, TARSKI:def 4;

        consider k be object such that

         B7: k in ( dom g1) & y = (g1 . k) by B6, FUNCT_1:def 3;

        reconsider k as Nat by B7;



         B8: k in ( dom g2) by B7, A8, FINSEQ_1:def 3;

        then (g2 . k) = ((g1 . k) \ A1) by A8;

        then x in (g2 . k) & (g2 . k) in ( rng g2) by B5, B6, B7, B8, XBOOLE_0:def 5, FUNCT_1: 3;

        hence x in ( union ( rng g2)) by TARSKI:def 4;

      end;

      then (( union ( rng g1)) \ A1) c= ( union ( rng g2));

      then (( union ( rng g1)) \ A1) = ( union ( rng g2)) by B4;

      hence (B \ A) in R by A5, A6, C1, FINSEQ_1: 58;

    end;

    theorem :: SRINGS_3:17



     lemma105: for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, A,B,R be set st R = ( DisUnion S) & A in R & B in R & A <> {} holds (B \ A) in R

    proof

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, A,B,R be set;

      assume that

       A1: R = ( DisUnion S) and

       A2: A in R & B in R & A <> {} ;

      consider A1 be Subset of X such that

       A3: A = A1 & ex F be disjoint_valued FinSequence of S st A1 = ( Union F) by A1, A2;

      consider f1 be disjoint_valued FinSequence of S such that

       A4: A1 = ( Union f1) by A3;

      consider B1 be Subset of X such that

       A5: B = B1 & ex F be disjoint_valued FinSequence of S st B1 = ( Union F) by A1, A2;

      reconsider R1 = R as non empty set by A2;

      defpred P[ Nat, object] means $2 = (B1 \ (f1 . $1));



       A7: for k be Nat st k in ( Seg ( len f1)) holds ex x be Element of R1 st P[k, x]

      proof

        let k be Nat;

        assume k in ( Seg ( len f1));

        then k in ( dom f1) by FINSEQ_1:def 3;

        then (f1 . k) in ( rng f1) & ( rng f1) c= S by FUNCT_1: 3;

        then (B1 \ (f1 . k)) in R1 by A1, A2, A5, lemma104;

        hence thesis;

      end;

      consider F be FinSequence of R1 such that

       A8: ( dom F) = ( Seg ( len f1)) & for k be Nat st k in ( Seg ( len f1)) holds P[k, (F . k)] from FINSEQ_1:sch 5( A7);

      now

        let x be object;

        assume

         C9: x in (B \ A);

        then x in B & not x in A by XBOOLE_0:def 5;

        then

         A10: for Y be set holds not x in Y or not Y in ( rng f1) by A3, A4, TARSKI:def 4;



         B1: for k be Nat st k in ( Seg ( len f1)) holds x in (F . k)

        proof

          let k be Nat;

          assume

           B2: k in ( Seg ( len f1));

          then

           B3: (F . k) = (B1 \ (f1 . k)) by A8;

          k in ( dom f1) by B2, FINSEQ_1:def 3;

          then not x in (f1 . k) by A10, FUNCT_1: 3;

          hence thesis by A5, C9, B3, XBOOLE_0:def 5;

        end;

        ( dom f1) <> {} by A2, A3, A4, ZFMISC_1: 2, RELAT_1: 42;

        then

        consider k be object such that

         B4: k in ( dom f1) by XBOOLE_0:def 1;

        reconsider k as Nat by B4;

        k in ( Seg ( len f1)) by B4, FINSEQ_1:def 3;

        then

         B5: ( rng F) <> {} by A8, FUNCT_1: 3;

        now

          let Y be set;

          assume Y in ( rng F);

          then

          consider k be object such that

           B6: k in ( dom F) & Y = (F . k) by FUNCT_1:def 3;

          reconsider k as Nat by B6;

          thus x in Y by A8, B6, B1;

        end;

        hence x in ( meet ( rng F)) by B5, SETFAM_1:def 1;

      end;

      then

       B7: (B \ A) c= ( meet ( rng F));

      now

        let x be object;

        assume

         B8: x in ( meet ( rng F));

        then

        consider Y be object such that

         B10: Y in ( rng F) by SETFAM_1: 1, XBOOLE_0:def 1;

        consider k be object such that

         B11: k in ( dom F) & Y = (F . k) by B10, FUNCT_1:def 3;

        reconsider k as Nat by B11;

        x in (F . k) by B8, B10, B11, SETFAM_1:def 1;

        then x in (B1 \ (f1 . k)) by A8, B11;

        then

         B12: x in B1 & not x in (f1 . k) by XBOOLE_0:def 5;

        now

          assume x in ( union ( rng f1));

          then

          consider Y be set such that

           B13: x in Y & Y in ( rng f1) by TARSKI:def 4;

          consider k be object such that

           B14: k in ( dom f1) & Y = (f1 . k) by B13, FUNCT_1:def 3;

          reconsider k as Nat by B14;



           B15: k in ( dom F) by B14, A8, FINSEQ_1:def 3;

          then (F . k) in ( rng F) by FUNCT_1: 3;

          then x in (F . k) by B8, SETFAM_1:def 1;

          then x in (B1 \ (f1 . k)) by B15, A8;

          hence contradiction by B13, B14, XBOOLE_0:def 5;

        end;

        hence x in (B \ A) by A3, A4, A5, B12, XBOOLE_0:def 5;

      end;

      then ( meet ( rng F)) c= (B \ A);

      then

       B16: (B \ A) = ( meet ( rng F)) by B7;

      defpred P[ Nat] means ( meet ( rng (F | $1))) in R;

      ( meet ( rng (F | 0 ))) in S & S c= R by A1, lemma100, SETFAM_1:def 8, SETFAM_1: 1;

      then

       C1: P[ 0 ];



       C2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         C3: P[k];

        per cases ;

          suppose

           C4: (k + 1) <= ( len F);

          (F | k) = ((F | (k + 1)) | k) by FINSEQ_1: 82, NAT_1: 11;

          then (F | (k + 1)) = ((F | k) ^ <*((F | (k + 1)) . (k + 1))*>) by C4, FINSEQ_1: 59, FINSEQ_3: 55;



          then

           C6: ( rng (F | (k + 1))) = (( rng (F | k)) \/ ( rng <*((F | (k + 1)) . (k + 1))*>)) by FINSEQ_1: 31

          .= (( rng (F | k)) \/ {((F | (k + 1)) . (k + 1))}) by FINSEQ_1: 38

          .= (( rng (F | k)) \/ {(F . (k + 1))}) by FINSEQ_3: 112;

          (k + 1) in ( dom F) by C4, FINSEQ_3: 25, NAT_1: 11;

          then

           C9: (F . (k + 1)) in ( rng F) & ( rng F) c= R1 by FUNCT_1: 3;

          then

           C7: (F . (k + 1)) in R;

          per cases ;

            suppose ( rng (F | k)) <> {} ;



            then

             C8: ( meet ( rng (F | (k + 1)))) = (( meet ( rng (F | k))) /\ ( meet {(F . (k + 1))})) by C6, SETFAM_1: 9

            .= (( meet ( rng (F | k))) /\ (F . (k + 1))) by SETFAM_1: 10;

            R is cap-closed by A1, lemma101;

            hence ( meet ( rng (F | (k + 1)))) in R by C3, C9, C8;

          end;

            suppose ( rng (F | k)) = {} ;

            hence ( meet ( rng (F | (k + 1)))) in R by C6, C7, SETFAM_1: 10;

          end;

        end;

          suppose (k + 1) > ( len F);

          then (F | k) = F & (F | (k + 1)) = F by FINSEQ_1: 58, NAT_1: 13;

          hence ( meet ( rng (F | (k + 1)))) in R by C3;

        end;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( C1, C2);

      then P[( len F)];

      hence (B \ A) in R by B16, FINSEQ_1: 58;

    end;

    theorem :: SRINGS_3:18

    for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X holds ( Ring_generated_by S) = ( DisUnion S)

    proof

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X;

      set R = ( DisUnion S);

      reconsider R as non empty Subset-Family of X;



       A0: S c= R by lemma100;



       A1: R is cap-closed by lemma101;

       A2:

      now

        let A,B be set;

        assume

         A3: A in R & B in R;

        then A <> {} implies (B \ A) in R by lemma105;

        hence (B \ A) in R by A3;

      end;

      then

       A4: R is diff-closed;

      now

        let A,B be set;

        assume A in R & B in R;

        then

         A5: (A \ B) in R & (B \ A) in R & (A /\ B) in R by A2, A1;

        ((A \ B) \/ (B \ A)) in R by A5, lemma102, XBOOLE_1: 82;

        then

         A6: (A \+\ B) in R by XBOOLE_0:def 6;

        ((A \+\ B) \/ (A /\ B)) in R by A5, A6, lemma102, XBOOLE_1: 103;

        hence (A \/ B) in R by XBOOLE_1: 93;

      end;

      then R is cup-closed;

      then

      reconsider R as non empty preBoolean Subset-Family of X by A4;



       A10: R in { Z where Z be non empty preBoolean Subset-Family of X : S c= Z } by A0;

      now

        let x be object;

        assume x in R;

        then

        consider A be Subset of X such that

         A8: x = A & ex F be disjoint_valued FinSequence of S st A = ( Union F);

        consider F be disjoint_valued FinSequence of S such that

         A9: A = ( Union F) by A8;

        for Y be set st Y in { Z where Z be non empty preBoolean Subset-Family of X : S c= Z } holds x in Y

        proof

          let Y be set;

          assume Y in { Z where Z be non empty preBoolean Subset-Family of X : S c= Z };

          then

          consider Z be non empty preBoolean Subset-Family of X such that

           A11: Y = Z & S c= Z;

          defpred P[ Nat] means ( union ( rng (F | $1))) in Z;



           X1: P[ 0 ] by SETFAM_1:def 8, ZFMISC_1: 2;



           X2: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume

             X3: P[k];

            per cases ;

              suppose

               C4: (k + 1) <= ( len F);

              (F | k) = ((F | (k + 1)) | k) by NAT_1: 11, FINSEQ_1: 82;

              then (F | (k + 1)) = ((F | k) ^ <*((F | (k + 1)) . (k + 1))*>) by C4, FINSEQ_1: 59, FINSEQ_3: 55;



              then ( rng (F | (k + 1))) = (( rng (F | k)) \/ ( rng <*((F | (k + 1)) . (k + 1))*>)) by FINSEQ_1: 31

              .= (( rng (F | k)) \/ {((F | (k + 1)) . (k + 1))}) by FINSEQ_1: 38

              .= (( rng (F | k)) \/ {(F . (k + 1))}) by FINSEQ_3: 112;



              then

               C6: ( union ( rng (F | (k + 1)))) = (( union ( rng (F | k))) \/ ( union {(F . (k + 1))})) by ZFMISC_1: 78

              .= (( union ( rng (F | k))) \/ (F . (k + 1)));

              (k + 1) in ( dom F) by C4, NAT_1: 11, FINSEQ_3: 25;

              then (F . (k + 1)) in ( rng F) & ( rng F) c= S by FUNCT_1: 3;

              then (F . (k + 1)) in Z by A11;

              hence P[(k + 1)] by X3, C6, FINSUB_1:def 1;

            end;

              suppose (k + 1) > ( len F);

              then (F | k) = F & (F | (k + 1)) = F by FINSEQ_1: 58, NAT_1: 13;

              hence P[(k + 1)] by X3;

            end;

          end;

          for k be Nat holds P[k] from NAT_1:sch 2( X1, X2);

          then P[( len F)];

          hence x in Y by A8, A9, A11, FINSEQ_1: 58;

        end;

        hence x in ( Ring_generated_by S) by A10, SETFAM_1:def 1;

      end;

      then R c= ( Ring_generated_by S);

      hence thesis by A10, SETFAM_1: 7;

    end;

    definition

      let X be set;

      :: SRINGS_3:def4

      mode SigmaRing of X -> non empty preBoolean Subset-Family of X means

      : DefSigmaRing: for F be SetSequence of X st ( rng F) c= it holds ( Union F) in it ;

      existence

      proof

        take ( bool X);

        thus thesis;

      end;

    end



     LemX: for X be set, S be SigmaRing of X holds S is sigma-multiplicative

    proof

      let X be set, S be SigmaRing of X;

      now

        let F be SetSequence of X;

        assume

         A1: ( rng F) c= S;

        then

         A2: ( Union F) in S by DefSigmaRing;

        reconsider UF = ( Union F) as Subset of X;

        now

          let x be object;

          assume

           BB: x in ( Intersection F);



           B0: ( Intersection F) c= UF by SETLIM_1: 9;

          now

            assume x in ( Union (UF (\) F));

            then

            consider m be Nat such that

             B1: x in ((UF (\) F) . m) by PROB_1: 12;

            x in (UF \ (F . m)) by B1, SETLIM_2:def 7;

            then not x in (F . m) by XBOOLE_0:def 5;

            hence contradiction by BB, PROB_1: 13;

          end;

          hence x in (UF \ ( Union (UF (\) F))) by BB, B0, XBOOLE_0:def 5;

        end;

        then

         B3: ( Intersection F) c= (UF \ ( Union (UF (\) F)));

        now

          let x be object;

          assume x in (UF \ ( Union (UF (\) F)));

          then

           C3: x in UF & not x in ( Union (UF (\) F)) by XBOOLE_0:def 5;

          hereby

            assume not x in ( Intersection F);

            then

            consider n be Nat such that

             C2: not x in (F . n) by PROB_1: 13;

            x in (UF \ (F . n)) by C3, C2, XBOOLE_0:def 5;

            then x in ((UF (\) F) . n) by SETLIM_2:def 7;

            hence contradiction by C3, PROB_1: 12;

          end;

        end;

        then (UF \ ( Union (UF (\) F))) c= ( Intersection F);

        then

         B5: ( Intersection F) = (( Union F) \ ( Union (UF (\) F))) by B3;

        now

          let x be object;

          assume x in ( rng (UF (\) F));

          then

          consider n be Element of NAT such that

           D1: x = ((UF (\) F) . n) by FUNCT_2: 113;



           D2: x = (UF \ (F . n)) by D1, SETLIM_2:def 7;

          (F . n) in ( rng F) by FUNCT_2: 112;

          hence x in S by A1, D2, A2, FINSUB_1:def 3;

        end;

        then ( rng (UF (\) F)) c= S;

        then ( Union (UF (\) F)) in S by DefSigmaRing;

        hence ( Intersection F) in S by A2, B5, FINSUB_1:def 3;

      end;

      hence S is sigma-multiplicative by PROB_1:def 6;

    end;

    registration

      let X be set;

      cluster -> sigma-multiplicative for SigmaRing of X;

      coherence by LemX;

    end

    definition

      let X be set, S be Subset-Family of X;

      :: SRINGS_3:def5

      func sigmaring S -> SigmaRing of X means

      : Defsigmaring: S c= it & for Z be set st S c= Z & Z is SigmaRing of X holds it c= Z;

      existence

      proof

        set V = { Z where Z be Subset-Family of X : S c= Z & Z is SigmaRing of X };

        set Y = ( meet V);

         A1:

        now

          let A be set;

          assume A in V;

          then ex Z be Subset-Family of X st A = Z & S c= Z & Z is SigmaRing of X;

          hence S c= A;

        end;

        for F be SetSequence of X st ( rng F) c= ( bool X) holds ( Union F) in ( bool X);

        then

        reconsider BX = ( bool X) as SigmaRing of X by DefSigmaRing;



         B1: BX in V;



         A3: Y c= ( bool X) by B1, SETFAM_1:def 1;

        now

          let x,y be set;

          assume

           C1: x in Y & y in Y;

          now

            let A be set;

            assume

             C3: A in V;

            then

            consider Z be Subset-Family of X such that

             C2: A = Z & S c= Z & Z is SigmaRing of X;

            x in A & y in A by C1, C3, SETFAM_1:def 1;

            hence (x \ y) in A by C2, FINSUB_1:def 3;

          end;

          hence (x \ y) in Y by B1, SETFAM_1:def 1;

        end;

        then

         A4: Y is diff-closed;

        now

          let x,y be set;

          assume

           F1: x in Y & y in Y;

          now

            let A be set;

            assume

             F2: A in V;

            then

            consider Z be Subset-Family of X such that

             F3: A = Z & S c= Z & Z is SigmaRing of X;

            x in A & y in A by F1, F2, SETFAM_1:def 1;

            hence (x \/ y) in A by F3, FINSUB_1:def 1;

          end;

          hence (x \/ y) in Y by B1, SETFAM_1:def 1;

        end;

        then

         E1: Y is cup-closed;

         A5:

        now

          let F be SetSequence of X;

          assume

           D1: ( rng F) c= Y;

          now

            let A be set;

            assume

             D2: A in V;

            then

            consider Z be Subset-Family of X such that

             D3: A = Z & S c= Z & Z is SigmaRing of X;

            Y c= A by D2, SETFAM_1: 3;

            then ( rng F) c= A by D1;

            hence ( Union F) in A by D3, DefSigmaRing;

          end;

          hence ( Union F) in Y by B1, SETFAM_1:def 1;

        end;

        now

          let A be set;

          assume A in V;

          then ex Z be Subset-Family of X st A = Z & S c= Z & Z is SigmaRing of X;

          hence {} in A by NE;

        end;

        then {} in Y by B1, SETFAM_1:def 1;

        then

        reconsider Y as SigmaRing of X by E1, A3, A4, A5, DefSigmaRing;

        take Y;

        for F be SetSequence of X st ( rng F) c= ( bool X) holds ( Union F) in ( bool X);

        then

        reconsider BX = ( bool X) as SigmaRing of X by DefSigmaRing;

        BX in V;

        hence S c= Y by A1, SETFAM_1: 5;

        hereby

          let Z be set;

          assume S c= Z & Z is SigmaRing of X;

          then Z in V;

          hence Y c= Z by SETFAM_1: 3;

        end;

      end;

      correctness ;

    end

    theorem :: SRINGS_3:19

    for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X holds ( sigmaring ( Ring_generated_by S)) = ( sigmaring S)

    proof

      let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X;



       A1: S c= ( Ring_generated_by S) by RingGen1;

      ( Ring_generated_by S) c= ( sigmaring ( Ring_generated_by S)) by Defsigmaring;

      then

       A2: S c= ( sigmaring ( Ring_generated_by S)) by A1;

      now

        let x be object;

        assume

         A3: x in ( Ring_generated_by S);

        S c= ( sigmaring S) by Defsigmaring;

        then ( sigmaring S) in { Z where Z be non empty preBoolean Subset-Family of X : S c= Z };

        hence x in ( sigmaring S) by A3, SETFAM_1:def 1;

      end;

      then ( Ring_generated_by S) c= ( sigmaring S);

      hence thesis by A2, Defsigmaring;

    end;

    begin

    definition

      let X be set;

      :: SRINGS_3:def6

      mode semialgebra_of_sets of X -> with_empty_element semi-diff-closed cap-closed Subset-Family of X means

      : Def1: X in it ;

      existence

      proof

        ( bool X) is with_empty_element semi-diff-closed cap-closed Subset-Family of X & X c= X;

        hence thesis;

      end;

    end

    theorem :: SRINGS_3:20

    for X be set, F be Field_Subset of X holds F is semialgebra_of_sets of X by Def1, PROB_1: 5;



     ExistAlgebra: for X be set, S be semialgebra_of_sets of X holds ex Y be non empty Field_Subset of X st Y = ( meet { Z where Z be Field_Subset of X : S c= Z })

    proof

      let X be set, S be semialgebra_of_sets of X;

      set V = { Z where Z be Field_Subset of X : S c= Z };



       A1: ( bool X) in V;

      then

      reconsider Y = ( meet V) as Subset-Family of X by SETFAM_1: 3;

      now

        let Z be set;

        assume Z in V;

        then ex S1 be Field_Subset of X st Z = S1 & S c= S1;

        hence {} in Z by SETFAM_1:def 8;

      end;

      then

       A2: Y is non empty by A1, SETFAM_1:def 1;

      now

        let A,B be set;

        assume

         B1: A in Y & B in Y;

        for Z be set st Z in V holds (A \/ B) in Z

        proof

          let Z be set;

          assume

           B2: Z in V;

          then

          consider Z1 be Field_Subset of X such that

           B3: Z = Z1 & S c= Z1;

          A in Z1 & B in Z1 by B1, B2, B3, SETFAM_1:def 1;

          hence (A \/ B) in Z by B3, FINSUB_1:def 1;

        end;

        hence (A \/ B) in Y by A1, SETFAM_1:def 1;

      end;

      then

       B4: Y is cup-closed;

      now

        let A be set;

        assume

         C1: A in Y;

        for Z be set st Z in V holds (X \ A) in Z

        proof

          let Z be set;

          assume

           C2: Z in V;

          then

          consider Z1 be Field_Subset of X such that

           C3: Z = Z1 & S c= Z1;

          A in Z1 & X in Z1 by Def1, C1, C2, C3, SETFAM_1:def 1;

          hence (X \ A) in Z by C3, FINSUB_1:def 3;

        end;

        hence (X \ A) in Y by A1, SETFAM_1:def 1;

      end;

      then Y is compl-closed by MEASURE1:def 1;

      hence thesis by A2, B4;

    end;

    definition

      let X be set, S be semialgebra_of_sets of X;

      :: SRINGS_3:def7

      func Field_generated_by S -> non empty Field_Subset of X equals ( meet { Z where Z be Field_Subset of X : S c= Z });

      correctness

      proof

        consider Y be non empty Field_Subset of X such that

         A1: Y = ( meet { Z where Z be Field_Subset of X : S c= Z }) by ExistAlgebra;

        thus thesis by A1;

      end;

    end

    theorem :: SRINGS_3:21



     FieldGen1: for X be set, P be semialgebra_of_sets of X holds P c= ( Field_generated_by P)

    proof

      let X be set, P be semialgebra_of_sets of X;

      set Y = { Z where Z be Field_Subset of X : P c= Z };



       A1: ( bool X) in Y;

      for A be set st A in Y holds P c= A

      proof

        let A be set;

        assume A in Y;

        then ex Z be Field_Subset of X st A = Z & P c= Z;

        hence P c= A;

      end;

      hence thesis by A1, SETFAM_1: 5;

    end;

    theorem :: SRINGS_3:22

    for X be set, S be semialgebra_of_sets of X holds ( Field_generated_by S) = ( DisUnion S)

    proof

      let X be set, S be semialgebra_of_sets of X;

      set R = ( DisUnion S);

      reconsider R as non empty Subset-Family of X;



       A0: S c= R by lemma100;



       A1: R is cap-closed by lemma101;

       A2:

      now

        let A,B be set;

        assume

         A3: A in R & B in R;

        then A <> {} implies (B \ A) in R by lemma105;

        hence (B \ A) in R by A3;

      end;

      then

       A4: R is diff-closed;

      now

        let A,B be set;

        assume A in R & B in R;

        then

         A5: (A \ B) in R & (B \ A) in R & (A /\ B) in R by A2, A1;

        ((A \ B) \/ (B \ A)) in R by A5, lemma102, XBOOLE_1: 82;

        then

         A6: (A \+\ B) in R by XBOOLE_0:def 6;

        ((A \+\ B) \/ (A /\ B)) in R by A5, A6, lemma102, XBOOLE_1: 103;

        hence (A \/ B) in R by XBOOLE_1: 93;

      end;

      then R is cup-closed;

      then

      reconsider R as non empty preBoolean Subset-Family of X by A4;

      now

        let A be set;

        assume

         C1: A in R;

        X in R by A0, Def1;

        hence (X \ A) in R by C1, FINSUB_1:def 3;

      end;

      then

       K2: R is compl-closed by MEASURE1:def 1;



       A10: R in { Z where Z be non empty Field_Subset of X : S c= Z } by A0, K2;

      now

        let x be object;

        assume x in R;

        then

        consider A be Subset of X such that

         A8: x = A & ex F be disjoint_valued FinSequence of S st A = ( Union F);

        consider F be disjoint_valued FinSequence of S such that

         A9: A = ( Union F) by A8;

        for Y be set st Y in { Z where Z be Field_Subset of X : S c= Z } holds x in Y

        proof

          let Y be set;

          assume Y in { Z where Z be Field_Subset of X : S c= Z };

          then

          consider Z be Field_Subset of X such that

           A11: Y = Z & S c= Z;

          defpred P[ Nat] means ( union ( rng (F | $1))) in Z;



           X1: P[ 0 ] by SETFAM_1:def 8, ZFMISC_1: 2;



           X2: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume

             X3: P[k];

            per cases ;

              suppose

               C4: (k + 1) <= ( len F);

              (F | k) = ((F | (k + 1)) | k) by NAT_1: 11, FINSEQ_1: 82;

              then (F | (k + 1)) = ((F | k) ^ <*((F | (k + 1)) . (k + 1))*>) by C4, FINSEQ_1: 59, FINSEQ_3: 55;



              then ( rng (F | (k + 1))) = (( rng (F | k)) \/ ( rng <*((F | (k + 1)) . (k + 1))*>)) by FINSEQ_1: 31

              .= (( rng (F | k)) \/ {((F | (k + 1)) . (k + 1))}) by FINSEQ_1: 38

              .= (( rng (F | k)) \/ {(F . (k + 1))}) by FINSEQ_3: 112;



              then

               C6: ( union ( rng (F | (k + 1)))) = (( union ( rng (F | k))) \/ ( union {(F . (k + 1))})) by ZFMISC_1: 78

              .= (( union ( rng (F | k))) \/ (F . (k + 1)));

              (k + 1) in ( dom F) by C4, NAT_1: 11, FINSEQ_3: 25;

              then (F . (k + 1)) in ( rng F) & ( rng F) c= S by FUNCT_1: 3;

              then (F . (k + 1)) in Z by A11;

              hence P[(k + 1)] by X3, C6, FINSUB_1:def 1;

            end;

              suppose (k + 1) > ( len F);

              then (F | k) = F & (F | (k + 1)) = F by FINSEQ_1: 58, NAT_1: 13;

              hence P[(k + 1)] by X3;

            end;

          end;

          for k be Nat holds P[k] from NAT_1:sch 2( X1, X2);

          then P[( len F)];

          hence x in Y by A8, A9, A11, FINSEQ_1: 58;

        end;

        hence x in ( Field_generated_by S) by A10, SETFAM_1:def 1;

      end;

      then R c= ( Field_generated_by S);

      hence thesis by A10, SETFAM_1: 7;

    end;

    theorem :: SRINGS_3:23

    for X be non empty set, S be semialgebra_of_sets of X holds ( sigma ( Field_generated_by S)) = ( sigma S)

    proof

      let X be non empty set, S be semialgebra_of_sets of X;



       A1: S c= ( Field_generated_by S) by FieldGen1;

      ( Field_generated_by S) c= ( sigma ( Field_generated_by S)) by PROB_1:def 9;

      then

       A2: S c= ( sigma ( Field_generated_by S)) by A1;

      now

        let x be object;

        assume

         A3: x in ( Field_generated_by S);

        S c= ( sigma S) by PROB_1:def 9;

        then ( sigma S) in { Z where Z be Field_Subset of X : S c= Z };

        hence x in ( sigma S) by A3, SETFAM_1:def 1;

      end;

      then ( Field_generated_by S) c= ( sigma S);

      hence thesis by A2, PROB_1:def 9;

    end;

    begin

    theorem :: SRINGS_3:24

    for X be set, S be set st S is SigmaField of X holds S is SigmaRing of X

    proof

      let X be set, S be set;

      assume

       A1: S is SigmaField of X;

      then for F be SetSequence of X st ( rng F) c= S holds ( Union F) in S by PROB_4: 4;

      hence S is SigmaRing of X by A1, DefSigmaRing;

    end;

    theorem :: SRINGS_3:25

    for X be set, S be set st S is SigmaRing of X & X in S holds S is SigmaField of X

    proof

      let X be set, S be set;

      assume that

       A1: S is SigmaRing of X and

       A2: X in S;

      reconsider S1 = S as non empty Subset-Family of X by A1;



       A3: S1 is diff-closed by A1;

       P1:

      now

        let A be Subset of X;

        assume A in S1;

        then (X \ A) in S1 by A2, A3;

        hence (A ` ) in S1 by SUBSET_1:def 4;

      end;

      X c= X;

      then

      reconsider X1 = X as Subset of X;

      now

        let A be SetSequence of X;

        assume

         P2: ( rng A) c= S1;

        now

          let a be object;

          assume a in ( rng ( Complement A));

          then

          consider n be Element of NAT such that

           P3: a = (( Complement A) . n) by FUNCT_2: 113;

          a = ((A . n) ` ) by P3, PROB_1:def 2;

          then

           P4: a = (X \ (A . n)) by SUBSET_1:def 4;

          (A . n) in ( rng A) by FUNCT_2: 4;

          hence a in S1 by P4, P2, A1, A2, FINSUB_1:def 3;

        end;

        then ( rng ( Complement A)) c= S1;

        then ( Union ( Complement A)) in S1 by A1, DefSigmaRing;

        then (X1 \ ( Union ( Complement A))) in S1 by A1, A2, FINSUB_1:def 3;

        then (( Union ( Complement A)) ` ) in S1 by SUBSET_1:def 4;

        hence ( Intersection A) in S1 by PROB_1:def 3;

      end;

      hence S is SigmaField of X by P1, PROB_1:def 1, PROB_1:def 6;

    end;

    theorem :: SRINGS_3:26

    for S be Subset-Family of REAL st S = { I where I be Subset of REAL : I is left_open_interval } holds S is with_empty_element semi-diff-closed cap-closed

    proof

      let S be Subset-Family of REAL ;

      assume S = { I where I be Subset of REAL : I is left_open_interval };

      then S is cap-closed & S is diff-finite-partition-closed with_empty_element & S is with_countable_Cover by SRINGS_2: 10;

      hence thesis by th10;

    end;



     INTERVAL01: for I be Subset of REAL st I = {} holds I is right_open_interval

    proof

      let I be Subset of REAL ;

      assume

       A1: I = {} ;

       0 in REAL by NUMBERS: 19;

      then [. 0 , 0 .[ is right_open_interval by NUMBERS: 31;

      hence I is right_open_interval by A1;

    end;



     INTERVAL02: for I,J be Subset of REAL st I is right_open_interval & J is right_open_interval & I meets J holds ex K,L be Subset of REAL st K is right_open_interval & L is right_open_interval & K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is right_open_interval & J is right_open_interval;

      then

      consider p be Real, q be R_eal such that

       A2: I = [.p, q.[;

      consider r be Real, s be R_eal such that

       A3: J = [.r, s.[ by A1;

      assume

       A9: I meets J;

      then

       A5: (I \ J) = ( [.p, r.[ \/ [.s, q.[) by A2, A3, XXREAL_1: 198;



       A10: q > r & s > p by A2, A3, A9, XXREAL_1: 96;

       A7:

      now

        assume s = -infty ;

        then s < r by XREAL_0:def 1, XXREAL_0: 12;

        then J = {} by A3, XXREAL_1: 27;

        hence contradiction by A9;

      end;

      per cases by A7, XXREAL_0: 14;

        suppose

         A8: s = +infty ;

        reconsider K = [.p, r.[ as Subset of REAL ;

        reconsider L = {} as Subset of REAL by XBOOLE_1: 2;

        take K, L;

        p in REAL & r in REAL by XREAL_0:def 1;

        hence K is right_open_interval by NUMBERS: 31;

        thus L is right_open_interval by INTERVAL01;

        thus K misses L;

        thus (I \ J) = (K \/ L) by A8, A5, XXREAL_1: 215;

      end;

        suppose

         B1: s in REAL & r <= s;

        then

        reconsider s1 = s as Real;

        reconsider K = [.p, r.[ as Subset of REAL ;

        reconsider L = [.s1, q.[ as Subset of REAL ;

        take K, L;

        r in REAL by XREAL_0:def 1;

        hence K is right_open_interval & L is right_open_interval by NUMBERS: 31;

        thus K misses L by B1, XXREAL_1: 96;

        thus (I \ J) = (K \/ L) by A9, A2, A3, XXREAL_1: 198;

      end;

        suppose

         C1: s in REAL & r > s;



         C2: ( min (p,s)) = p & ( max (r,q)) = q by A2, A3, A9, XXREAL_1: 96, XXREAL_0:def 9, XXREAL_0:def 10;

        reconsider s1 = s as Real by C1;

        s1 < q by A2, A3, A9, XXREAL_1: 96, C1, XXREAL_0: 2;

        then s1 in [.p, r.[ & s1 in [.s1, q.[ by A10, C1;

        then

         C3: [.p, r.[ meets [.s, q.[ by XBOOLE_0:def 4;

        reconsider K = [.p, q.[ as Subset of REAL ;

        reconsider L = {} as Subset of REAL by XBOOLE_1: 2;

        take K, L;

        thus K is right_open_interval;

        thus L is right_open_interval by INTERVAL01;

        thus K misses L;

        thus (I \ J) = (K \/ L) by C3, C2, A5, XXREAL_1: 162;

      end;

    end;



     OOdif: for I,J be Subset of REAL st I is open_interval & J is open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is open_interval & J is open_interval & I meets J;

      then

      consider p,q be R_eal such that

       A2: I = ].p, q.[;

      consider r,s be R_eal such that

       A3: J = ].r, s.[ by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p < q & r < s & p < s & r < q by A1, A2, A3, XXREAL_1: 28, XXREAL_1: 275;



       A7: r <> +infty & s <> -infty by A1, A3, XXREAL_1: 275, XXREAL_0: 3, XXREAL_0: 5;

      per cases by A7, XXREAL_0: 14;

        suppose r in REAL & s in REAL ;

        then

        reconsider r1 = r, s1 = s as Real;

        reconsider K = ].p, r1.], L = [.s1, q.[ as Subset of REAL ;

        K is left_open_interval & L is right_open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 279, XXREAL_1: 297;

      end;

        suppose

         A8: r = -infty & s in REAL ;

        then

         A9: ].p, r.] = {} & ].p, r.[ = {} by XXREAL_0: 5, XXREAL_1: 26, XXREAL_1: 28;

        reconsider s1 = s as Real by A8;

        reconsider K = ].p, r.[, L = [.s1, q.[ as Subset of REAL ;

        K is open_interval & L is right_open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 297, A9;

      end;

        suppose

         A10: r in REAL & s = +infty ;

        then

         A11: [.s, q.[ = {} & ].s, q.[ = {} by XXREAL_0: 3, XXREAL_1: 27, XXREAL_1: 28;

        reconsider r1 = r as Real by A10;

        reconsider K = ].p, r1.], L = ].s, q.[ as Subset of REAL ;

        K is left_open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 297, A11;

      end;

        suppose r = -infty & s = +infty ;

        then

         A12: ].p, r.] = {} & ].p, r.[ = {} & [.s, q.[ = {} & ].s, q.[ = {} by XXREAL_0: 5, XXREAL_0: 3, XXREAL_1: 26, XXREAL_1: 27, XXREAL_1: 28;

        reconsider K = ].p, r.[, L = ].s, q.[ as Subset of REAL ;

        K is open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 297, A12;

      end;

    end;



     COdif: for I,J be Subset of REAL st I is closed_interval & J is open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is closed_interval & J is open_interval & I meets J;

      then

      consider p,q be Real such that

       A2: I = [.p, q.];

      consider r,s be R_eal such that

       A3: J = ].r, s.[ by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p <= q & r < s & r < q & p < s by A1, A2, A3, XXREAL_1: 29, XXREAL_1: 28, XXREAL_1: 89, XXREAL_1: 93;



       A7: r <> +infty & s <> -infty by A1, A3, XXREAL_1: 89, XXREAL_1: 93, XXREAL_0: 3, XXREAL_0: 5;

      per cases by A7, XXREAL_0: 14;

        suppose r in REAL & s in REAL ;

        then

        reconsider r1 = r, s1 = s as Real;

        reconsider K = [.p, r1.], L = [.s1, q.] as Subset of REAL ;

        K is closed_interval & L is closed_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 300, XXREAL_1: 278;

      end;

        suppose

         A8: r = -infty & s in REAL ;

        r < p by A8, XREAL_0:def 1, XXREAL_0: 12;

        then

         A9: [.p, r.] = {} & ].p, r.[ = {} by XXREAL_1: 28, XXREAL_1: 29;

        reconsider s1 = s as Real by A8;

        reconsider K = ].p, r.[, L = [.s1, q.] as Subset of REAL ;

        p is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is closed_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 300, A9;

      end;

        suppose

         A10: r in REAL & s = +infty ;

        then q < s by XREAL_0:def 1, XXREAL_0: 9;

        then

         A11: [.s, q.] = {} & ].s, q.[ = {} by XXREAL_1: 28, XXREAL_1: 29;

        reconsider r1 = r as Real by A10;

        reconsider K = [.p, r1.], L = ].s, q.[ as Subset of REAL ;

        q is R_eal by XXREAL_0:def 1;

        then K is closed_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 300, A11;

      end;

        suppose

         A13: r = -infty & s = +infty ;

        r < p & q < s by A13, XREAL_0:def 1, XXREAL_0: 9, XXREAL_0: 12;

        then

         A12: [.p, r.] = {} & ].p, r.[ = {} & [.s, q.] = {} & ].s, q.[ = {} by XXREAL_1: 28, XXREAL_1: 29;

        reconsider K = ].p, r.[, L = ].s, q.[ as Subset of REAL ;

        p is R_eal & q is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 300, A12;

      end;

    end;



     ROdif: for I,J be Subset of REAL st I is right_open_interval & J is open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is right_open_interval & J is open_interval & I meets J;

      then

      consider p be Real, q be R_eal such that

       A2: I = [.p, q.[;

      consider r,s be R_eal such that

       A3: J = ].r, s.[ by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p < q & r < s & r < q & p <= s by A1, A2, A3, XXREAL_1: 27, XXREAL_1: 28, XXREAL_1: 94, XXREAL_1: 273;



       A7: r <> +infty & s <> -infty by A1, A3, XXREAL_1: 94, XXREAL_1: 273, XXREAL_0: 3, XXREAL_0: 5;

      per cases by A7, XXREAL_0: 14;

        suppose r in REAL & s in REAL ;

        then

        reconsider r1 = r, s1 = s as Real;

        reconsider K = [.p, r1.], L = [.s1, q.[ as Subset of REAL ;

        K is closed_interval & L is right_open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 298, XXREAL_1: 277;

      end;

        suppose

         A8: r = -infty & s in REAL ;

        then r < p by XREAL_0:def 1, XXREAL_0: 12;

        then

         A9: [.p, r.] = {} & ].p, r.[ = {} by XXREAL_1: 28, XXREAL_1: 29;

        reconsider s1 = s as Real by A8;

        reconsider K = ].p, r.[, L = [.s1, q.[ as Subset of REAL ;

        p is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is right_open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 298, A9;

      end;

        suppose

         A10: r in REAL & s = +infty ;

        then

         A11: [.s, q.[ = {} & ].s, q.[ = {} by XXREAL_0: 3, XXREAL_1: 27, XXREAL_1: 28;

        reconsider r1 = r as Real by A10;

        reconsider K = [.p, r1.], L = ].s, q.[ as Subset of REAL ;

        K is closed_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 298, A11;

      end;

        suppose r = -infty & s = +infty ;

        then r < p & q <= s by XREAL_0:def 1, XXREAL_0: 3, XXREAL_0: 12;

        then

         A12: [.p, r.] = {} & ].p, r.[ = {} & [.s, q.[ = {} & ].s, q.[ = {} by XXREAL_1: 27, XXREAL_1: 28, XXREAL_1: 29;

        reconsider K = ].p, r.[, L = ].s, q.[ as Subset of REAL ;

        p is R_eal & q is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 298, A12;

      end;

    end;



     LOdif: for I,J be Subset of REAL st I is left_open_interval & J is open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is left_open_interval & J is open_interval & I meets J;

      then

      consider p be R_eal, q be Real such that

       A2: I = ].p, q.];

      consider r,s be R_eal such that

       A3: J = ].r, s.[ by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p < q & r < s & r < q & p < s by A1, A2, A3, XXREAL_1: 26, XXREAL_1: 28, XXREAL_1: 276, XXREAL_1: 91;



       A7: r <> +infty & s <> -infty by A1, A3, XXREAL_1: 276, XXREAL_1: 91, XXREAL_0: 3, XXREAL_0: 5;

      per cases by A7, XXREAL_0: 14;

        suppose r in REAL & s in REAL ;

        then

        reconsider r1 = r, s1 = s as Real;

        reconsider K = ].p, r1.], L = [.s1, q.] as Subset of REAL ;

        K is left_open_interval & L is closed_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 299, XXREAL_1: 280;

      end;

        suppose

         A8: r = -infty & s in REAL ;

        then

         A9: ].p, r.] = {} & ].p, r.[ = {} by XXREAL_0: 5, XXREAL_1: 26, XXREAL_1: 28;

        reconsider s1 = s as Real by A8;

        reconsider K = ].p, r.[, L = [.s1, q.] as Subset of REAL ;

        K is open_interval & L is closed_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 299, A9;

      end;

        suppose

         A10: r in REAL & s = +infty ;

        q < s by A10, XREAL_0:def 1, XXREAL_0: 9;

        then

         A11: [.s, q.] = {} & ].s, q.[ = {} by XXREAL_1: 28, XXREAL_1: 29;

        reconsider r1 = r as Real by A10;

        reconsider K = ].p, r1.], L = ].s, q.[ as Subset of REAL ;

        q is R_eal by XXREAL_0:def 1;

        then K is left_open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 299, A11;

      end;

        suppose

         A13: r = -infty & s = +infty ;

        r <= p & q < s by A13, XREAL_0:def 1, XXREAL_0: 5, XXREAL_0: 9;

        then

         A12: ].p, r.] = {} & ].p, r.[ = {} & [.s, q.] = {} & ].s, q.[ = {} by XXREAL_1: 26, XXREAL_1: 28, XXREAL_1: 29;

        reconsider K = ].p, r.[, L = ].s, q.[ as Subset of REAL ;

        p is R_eal & q is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 299, A12;

      end;

    end;



     OCdif: for I,J be Subset of REAL st I is open_interval & J is closed_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is open_interval & J is closed_interval & I meets J;

      then

      consider p,q be R_eal such that

       A2: I = ].p, q.[;

      consider r,s be Real such that

       A3: J = [.r, s.] by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p < q & r <= s & p < s & r < q by A1, A2, A3, XXREAL_1: 28, XXREAL_1: 29, XXREAL_1: 89, XXREAL_1: 93;

      reconsider K = ].p, r.[, L = ].s, q.[ as Subset of REAL ;

      r is R_eal & s is R_eal by XXREAL_0:def 1;

      then K is open_interval & L is open_interval;

      then

      reconsider K, L as Interval;

      take K, L;

      thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 309, XXREAL_1: 275;

    end;



     CCdif: for I,J be Subset of REAL st I is closed_interval & J is closed_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is closed_interval & J is closed_interval & I meets J;

      then

      consider p,q be Real such that

       A2: I = [.p, q.];

      consider r,s be Real such that

       A3: J = [.r, s.] by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p <= q & r <= s & p <= s & r <= q by A1, A2, A3, XXREAL_1: 29, XXREAL_1: 278;

      reconsider K = [.p, r.[, L = ].s, q.] as Subset of REAL ;

      r is R_eal & s is R_eal by XXREAL_0:def 1;

      then K is right_open_interval & L is left_open_interval;

      then

      reconsider K, L as Interval;

      take K, L;

      thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 312, XXREAL_1: 274;

    end;



     RCdif: for I,J be Subset of REAL st I is right_open_interval & J is closed_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is right_open_interval & J is closed_interval & I meets J;

      then

      consider p be Real, q be R_eal such that

       A2: I = [.p, q.[;

      consider r,s be Real such that

       A3: J = [.r, s.] by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p < q & r <= s & p <= s & r < q by A1, A2, A3, XXREAL_1: 27, XXREAL_1: 29, XXREAL_1: 95, XXREAL_1: 277;

      reconsider K = [.p, r.[, L = ].s, q.[ as Subset of REAL ;

      r is R_eal & s is R_eal by XXREAL_0:def 1;

      then K is right_open_interval & L is open_interval;

      then

      reconsider K, L as Interval;

      take K, L;

      thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 310, XXREAL_1: 273;

    end;



     LCdif: for I,J be Subset of REAL st I is left_open_interval & J is closed_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is left_open_interval & J is closed_interval & I meets J;

      then

      consider p be R_eal, q be Real such that

       A2: I = ].p, q.];

      consider r,s be Real such that

       A3: J = [.r, s.] by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p < q & r <= s & p < s & r <= q by A1, A2, A3, XXREAL_1: 26, XXREAL_1: 29, XXREAL_1: 90, XXREAL_1: 280;

      reconsider K = ].p, r.[, L = ].s, q.] as Subset of REAL ;

      r is R_eal & s is R_eal by XXREAL_0:def 1;

      then K is open_interval & L is left_open_interval;

      then

      reconsider K, L as Interval;

      take K, L;

      thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 311, XXREAL_1: 276;

    end;



     ORdif: for I,J be Subset of REAL st I is open_interval & J is right_open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is open_interval & J is right_open_interval & I meets J;

      then

      consider p,q be R_eal such that

       A2: I = ].p, q.[;

      consider r be Real, s be R_eal such that

       A3: J = [.r, s.[ by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p < q & r <= s & p < s & r <= q by A1, A2, A3, XXREAL_1: 27, XXREAL_1: 28, XXREAL_1: 94, XXREAL_1: 273;



       A7: s <> -infty by A1, A3, XXREAL_1: 273, XXREAL_0: 5;

      per cases by A7, XXREAL_0: 14;

        suppose s = +infty ;

        then

         A8: [.s, q.[ = {} & ].s, q.[ = {} by XXREAL_0: 3, XXREAL_1: 27, XXREAL_1: 28;

        reconsider K = ].p, r.[, L = ].s, q.[ as Subset of REAL ;

        r is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 301, A8;

      end;

        suppose s in REAL ;

        then

        reconsider s1 = s as Real;

        reconsider K = ].p, r.[, L = [.s1, q.[ as Subset of REAL ;

        r is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is right_open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, XXREAL_1: 94, XXREAL_1: 301, A2, A3;

      end;

    end;



     CRdif: for I,J be Subset of REAL st I is closed_interval & J is right_open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is closed_interval & J is right_open_interval & I meets J;

      then

      consider p,q be Real such that

       A2: I = [.p, q.];

      consider r be Real, s be R_eal such that

       A3: J = [.r, s.[ by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p <= q & r < s & p < s & r <= q by A1, A2, A3, XXREAL_1: 29, XXREAL_1: 27, XXREAL_1: 95, XXREAL_1: 277;



       A7: s <> -infty by A1, A3, XXREAL_1: 95, XXREAL_0: 5;

      per cases by A7, XXREAL_0: 14;

        suppose

         B1: s = +infty ;

        q < s by B1, XREAL_0:def 1, XXREAL_0: 9;

        then

         A8: [.s, q.] = {} & ].s, q.[ = {} by XXREAL_1: 29, XXREAL_1: 28;

        reconsider K = [.p, r.[, L = ].s, q.[ as Subset of REAL ;

        r is R_eal & q is R_eal by XXREAL_0:def 1;

        then K is right_open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 304, A8;

      end;

        suppose s in REAL ;

        then

        reconsider s1 = s as Real;

        reconsider K = [.p, r.[, L = [.s1, q.] as Subset of REAL ;

        r is R_eal by XXREAL_0:def 1;

        then K is right_open_interval & L is closed_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 304, XXREAL_1: 95;

      end;

    end;



     RRdif: for I,J be Subset of REAL st I is right_open_interval & J is right_open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume I is right_open_interval & J is right_open_interval & I meets J;

      then

      consider K,L be Subset of REAL such that

       A2: K is right_open_interval & L is right_open_interval & K misses L & (I \ J) = (K \/ L) by INTERVAL02;

      reconsider K, L as Interval by A2;

      thus thesis by A2;

    end;



     LRdif: for I,J be Subset of REAL st I is left_open_interval & J is right_open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is left_open_interval & J is right_open_interval & I meets J;

      then

      consider p be R_eal, q be Real such that

       A2: I = ].p, q.];

      consider r be Real, s be R_eal such that

       A3: J = [.r, s.[ by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p < q & r <= s & p < s & r <= q by A1, A2, A3, XXREAL_1: 26, XXREAL_1: 27, XXREAL_1: 274, XXREAL_1: 279;



       A7: s <> -infty by A1, A3, XXREAL_1: 274, XXREAL_0: 5;

      per cases by A7, XXREAL_0: 14;

        suppose

         B1: s = +infty ;

        q < s by B1, XREAL_0:def 1, XXREAL_0: 9;

        then

         A8: [.s, q.] = {} & ].s, q.[ = {} by XXREAL_1: 29, XXREAL_1: 28;

        reconsider K = ].p, r.[, L = ].s, q.[ as Subset of REAL ;

        r is R_eal & q is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 303, A8;

      end;

        suppose s in REAL ;

        then

        reconsider s1 = s as Real;

        reconsider K = ].p, r.[, L = [.s1, q.] as Subset of REAL ;

        r is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is closed_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 303, XXREAL_1: 93;

      end;

    end;



     OLdif: for I,J be Subset of REAL st I is open_interval & J is left_open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is open_interval & J is left_open_interval & I meets J;

      then

      consider p,q be R_eal such that

       A2: I = ].p, q.[;

      consider r be R_eal, s be Real such that

       A3: J = ].r, s.] by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p < q & r < s & q > r & s > p by A1, A2, A3, XXREAL_1: 28, XXREAL_1: 26, XXREAL_1: 276, XXREAL_1: 91;



       A7: r <> +infty by A1, A3, XXREAL_1: 276, XXREAL_0: 3;

      per cases by A7, XXREAL_0: 14;

        suppose r = -infty ;

        then

         A8: ].p, r.] = {} & ].p, r.[ = {} by XXREAL_0: 5, XXREAL_1: 26, XXREAL_1: 28;

        reconsider K = ].p, r.[, L = ].s, q.[ as Subset of REAL ;

        s is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 305, A8;

      end;

        suppose r in REAL ;

        then

        reconsider r1 = r as Real;

        reconsider K = ].p, r1.], L = ].s, q.[ as Subset of REAL ;

        s is R_eal by XXREAL_0:def 1;

        then K is left_open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 305, XXREAL_1: 91;

      end;

    end;



     CLdif: for I,J be Subset of REAL st I is closed_interval & J is left_open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is closed_interval & J is left_open_interval & I meets J;

      then

      consider p,q be Real such that

       A2: I = [.p, q.];

      consider r be R_eal, s be Real such that

       A3: J = ].r, s.] by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p <= q & r < s & q > r & s >= p by A1, A2, A3, XXREAL_1: 29, XXREAL_1: 26, XXREAL_1: 90, XXREAL_1: 280;



       A7: r <> +infty by A1, A3, XXREAL_1: 90, XXREAL_0: 3;

      per cases by A7, XXREAL_0: 14;

        suppose

         B1: r = -infty ;

        r < p by B1, XREAL_0:def 1, XXREAL_0: 12;

        then

         A8: [.p, r.] = {} & ].p, r.[ = {} by XXREAL_1: 29, XXREAL_1: 28;

        reconsider K = ].p, r.[, L = ].s, q.] as Subset of REAL ;

        p is R_eal & s is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is left_open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 308, A8;

      end;

        suppose r in REAL ;

        then

        reconsider r1 = r as Real;

        reconsider K = [.p, r1.], L = ].s, q.] as Subset of REAL ;

        s is R_eal by XXREAL_0:def 1;

        then K is closed_interval & L is left_open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 308, XXREAL_1: 90;

      end;

    end;



     RLdif: for I,J be Subset of REAL st I is right_open_interval & J is left_open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is right_open_interval & J is left_open_interval & I meets J;

      then

      consider p be Real, q be R_eal such that

       A2: I = [.p, q.[;

      consider r be R_eal, s be Real such that

       A3: J = ].r, s.] by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p <= q & r < s & q > r & s >= p by A1, A2, A3, XXREAL_1: 27, XXREAL_1: 26, XXREAL_1: 274, XXREAL_1: 279;



       A7: r <> +infty by A1, A3, XXREAL_1: 274, XXREAL_0: 3;

      per cases by A7, XXREAL_0: 14;

        suppose

         B1: r = -infty ;

        r < p by B1, XREAL_0:def 1, XXREAL_0: 12;

        then

         A8: [.p, r.] = {} & ].p, r.[ = {} by XXREAL_1: 29, XXREAL_1: 28;

        reconsider K = ].p, r.[, L = ].s, q.[ as Subset of REAL ;

        p is R_eal & s is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 306, A8;

      end;

        suppose r in REAL ;

        then

        reconsider r1 = r as Real;

        reconsider K = [.p, r1.], L = ].s, q.[ as Subset of REAL ;

        s is R_eal by XXREAL_0:def 1;

        then K is closed_interval & L is open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A2, A3, XXREAL_1: 306, XXREAL_1: 89;

      end;

    end;



     LLdif: for I,J be Subset of REAL st I is left_open_interval & J is left_open_interval & I meets J holds ex K,L be Interval st K misses L & (I \ J) = (K \/ L)

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is left_open_interval & J is left_open_interval & I meets J;

      then

      consider p be R_eal, q be Real such that

       A2: I = ].p, q.];

      consider r be R_eal, s be Real such that

       A3: J = ].r, s.] by A1;

      I <> {} & J <> {} by A1;

      then

       A4: p < q & r < s & q > r & s > p by A1, A2, A3, XXREAL_1: 26, XXREAL_1: 92;



       A7: r <> +infty by A1, A3, XXREAL_1: 92, XXREAL_0: 3;

      per cases by A7, XXREAL_0: 14;

        suppose r = -infty ;

        then

         A8: ].p, r.] = {} & ].p, r.[ = {} by XXREAL_0: 5, XXREAL_1: 26, XXREAL_1: 28;

        reconsider K = ].p, r.[, L = ].s, q.] as Subset of REAL ;

        p is R_eal & s is R_eal by XXREAL_0:def 1;

        then K is open_interval & L is left_open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A8, A1, A2, A3, XXREAL_1: 199;

      end;

        suppose r in REAL ;

        then

        reconsider r1 = r as Real;

        reconsider K = ].p, r1.], L = ].s, q.] as Subset of REAL ;

        s is R_eal by XXREAL_0:def 1;

        then K is left_open_interval & L is left_open_interval;

        then

        reconsider K, L as Interval;

        take K, L;

        thus K misses L & (I \ J) = (K \/ L) by A4, A1, A2, A3, XXREAL_1: 199, XXREAL_1: 92;

      end;

    end;



     INTERVAL03: for I,J be Subset of REAL st I is right_open_interval & J is right_open_interval holds (I /\ J) is right_open_interval

    proof

      let I,J be Subset of REAL ;

      assume

       A1: I is right_open_interval & J is right_open_interval;

      then

      consider p be Real, q be R_eal such that

       A2: I = [.p, q.[;

      consider r be Real, s be R_eal such that

       A3: J = [.r, s.[ by A1;



       A4: ( min (s,q)) is R_eal by XXREAL_0:def 1;

      (I /\ J) = [.( max (r,p)), ( min (s,q)).[ by A2, A3, XXREAL_1: 139;

      hence (I /\ J) is right_open_interval by A4;

    end;



     OOmeet: for I,J be Interval st I is open_interval & J is open_interval & I meets J holds (I /\ J) is Interval

    proof

      let I,J be Interval;

      assume

       A1: I is open_interval & J is open_interval & I meets J;

      then

      consider p,q be R_eal such that

       A2: I = ].p, q.[;

      consider r,s be R_eal such that

       A3: J = ].r, s.[ by A1;



       A4: (I /\ J) = ].( max (p,r)), ( min (q,s)).[ by A2, A3, XXREAL_1: 142;

      ( max (p,r)) is R_eal & ( min (q,s)) is R_eal by XXREAL_0:def 1;

      then (I /\ J) is open_interval by A4;

      hence (I /\ J) is Interval;

    end;



     OCmeet: for I,J be Interval st I is open_interval & J is closed_interval & I meets J holds (I /\ J) is Interval

    proof

      let I,J be Interval;

      assume

       A1: I is open_interval & J is closed_interval & I meets J;

      then

      consider p,q be R_eal such that

       A2: I = ].p, q.[;

      consider r,s be Real such that

       A3: J = [.r, s.] by A1;

      per cases ;

        suppose p < r & s < q;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 47, XBOOLE_1: 28;

      end;

        suppose p < r & q <= s;

        then (I /\ J) = [.r, q.[ by A2, A3, XXREAL_1: 148;

        then (I /\ J) is right_open_interval;

        hence (I /\ J) is Interval;

      end;

        suppose p >= r & q > s;

        then (I /\ J) = ].p, s.] by A2, A3, XXREAL_1: 149;

        then (I /\ J) is left_open_interval;

        hence (I /\ J) is Interval;

      end;

        suppose p >= r & q <= s;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 37, XBOOLE_1: 28;

      end;

    end;



     ORmeet: for I,J be Interval st I is open_interval & J is right_open_interval & I meets J holds (I /\ J) is Interval

    proof

      let I,J be Interval;

      assume

       A1: I is open_interval & J is right_open_interval & I meets J;

      then

      consider p,q be R_eal such that

       A2: I = ].p, q.[;

      consider r be Real, s be R_eal such that

       A3: J = [.r, s.[ by A1;

      per cases ;

        suppose p < r & q <= s;

        then (I /\ J) = [.r, q.[ by A2, A3, XXREAL_1: 154;

        then (I /\ J) is right_open_interval;

        hence (I /\ J) is Interval;

      end;

        suppose p < r & s <= q;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 48, XBOOLE_1: 28;

      end;

        suppose p >= r & q >= s;

        then (I /\ J) = ].p, s.[ by A2, A3, XXREAL_1: 155;

        then (I /\ J) is open_interval;

        hence (I /\ J) is Interval;

      end;

        suppose r <= p & q < s;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 45, XBOOLE_1: 28;

      end;

    end;



     OLmeet: for I,J be Interval st I is open_interval & J is left_open_interval & I meets J holds (I /\ J) is Interval

    proof

      let I,J be Interval;

      assume

       A1: I is open_interval & J is left_open_interval & I meets J;

      then

      consider p,q be R_eal such that

       A2: I = ].p, q.[;

      consider r be R_eal, s be Real such that

       A3: J = ].r, s.] by A1;

      per cases ;

        suppose p <= r & q <= s;

        then (I /\ J) = ].r, q.[ by A2, A3, XXREAL_1: 158;

        then (I /\ J) is open_interval;

        hence (I /\ J) is Interval;

      end;

        suppose p <= r & s < q;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 49, XBOOLE_1: 28;

      end;

        suppose p >= r & q > s;

        then (I /\ J) = ].p, s.] by A2, A3, XXREAL_1: 159;

        then (I /\ J) is left_open_interval;

        hence (I /\ J) is Interval;

      end;

        suppose p >= r & q <= s;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 41, XBOOLE_1: 28;

      end;

    end;



     CCmeet: for I,J be Interval st I is closed_interval & J is closed_interval & I meets J holds (I /\ J) is Interval

    proof

      let I,J be Interval;

      assume

       A1: I is closed_interval & J is closed_interval & I meets J;

      then

      consider p,q be Real such that

       A2: I = [.p, q.];

      consider r,s be Real such that

       A3: J = [.r, s.] by A1;



       A4: (I /\ J) = [.( max (r,p)), ( min (s,q)).] by A2, A3, XXREAL_1: 140;

      (I /\ J) is closed_interval by A4;

      hence (I /\ J) is Interval;

    end;



     CRmeet: for I,J be Interval st I is closed_interval & J is right_open_interval & I meets J holds (I /\ J) is Interval

    proof

      let I,J be Interval;

      assume

       A1: I is closed_interval & J is right_open_interval & I meets J;

      then

      consider p,q be Real such that

       A2: I = [.p, q.];

      consider r be Real, s be R_eal such that

       A3: J = [.r, s.[ by A1;

      per cases ;

        suppose r <= p & s <= q;

        then (I /\ J) = [.p, s.[ by A2, A3, XXREAL_1: 144;

        then (I /\ J) is right_open_interval;

        hence (I /\ J) is Interval;

      end;

        suppose r <= p & s > q;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 43, XBOOLE_1: 28;

      end;

        suppose r > p & s <= q;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 35, XBOOLE_1: 28;

      end;

        suppose r > p & s > q;

        then (I /\ J) = [.r, q.] by A2, A3, XXREAL_1: 145;

        then (I /\ J) is closed_interval;

        hence (I /\ J) is Interval;

      end;

    end;



     CLmeet: for I,J be Interval st I is closed_interval & J is left_open_interval & I meets J holds (I /\ J) is Interval

    proof

      let I,J be Interval;

      assume

       A1: I is closed_interval & J is left_open_interval & I meets J;

      then

      consider p,q be Real such that

       A2: I = [.p, q.];

      consider r be R_eal, s be Real such that

       A3: J = ].r, s.] by A1;

      per cases ;

        suppose r < p & s <= q;

        then (I /\ J) = [.p, s.] by A2, A3, XXREAL_1: 146;

        then (I /\ J) is closed_interval;

        hence (I /\ J) is Interval;

      end;

        suppose r < p & q < s;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 39, XBOOLE_1: 28;

      end;

        suppose p <= r & q <= s;

        then (I /\ J) = ].r, q.] by A2, A3, XXREAL_1: 147;

        then (I /\ J) is left_open_interval;

        hence (I /\ J) is Interval;

      end;

        suppose p <= r & s < q;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 36, XBOOLE_1: 28;

      end;

    end;



     RRmeet: for I,J be Interval st I is right_open_interval & J is right_open_interval & I meets J holds (I /\ J) is Interval

    proof

      let I,J be Interval;

      assume

       A1: I is right_open_interval & J is right_open_interval & I meets J;

      then

      consider p be Real, q be R_eal such that

       A2: I = [.p, q.[;

      consider r be Real, s be R_eal such that

       A3: J = [.r, s.[ by A1;



       A4: (I /\ J) = [.( max (r,p)), ( min (s,q)).[ by A2, A3, XXREAL_1: 139;

      ( max (p,r)) is Real & ( min (q,s)) is R_eal by XXREAL_0:def 1;

      then (I /\ J) is right_open_interval by A4;

      hence (I /\ J) is Interval;

    end;



     RLmeet: for I,J be Interval st I is right_open_interval & J is left_open_interval & I meets J holds (I /\ J) is Interval

    proof

      let I,J be Interval;

      assume

       A1: I is right_open_interval & J is left_open_interval & I meets J;

      then

      consider p be Real, q be R_eal such that

       A2: I = [.p, q.[;

      consider r be R_eal, s be Real such that

       A3: J = ].r, s.] by A1;

      per cases ;

        suppose r < p & s < q;

        then (I /\ J) = [.p, s.] by A2, A3, XXREAL_1: 152;

        then (I /\ J) is closed_interval;

        hence (I /\ J) is Interval;

      end;

        suppose r < p & q <= s;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 40, XBOOLE_1: 28;

      end;

        suppose p <= r & q <= s;

        then (I /\ J) = ].r, q.[ by A2, A3, XXREAL_1: 153;

        then (I /\ J) is open_interval;

        hence (I /\ J) is Interval;

      end;

        suppose p <= r & s < q;

        hence (I /\ J) is Interval by A2, A3, XXREAL_1: 44, XBOOLE_1: 28;

      end;

    end;



     LLmeet: for I,J be Interval st I is left_open_interval & J is left_open_interval & I meets J holds (I /\ J) is Interval

    proof

      let I,J be Interval;

      assume

       A1: I is left_open_interval & J is left_open_interval & I meets J;

      then

      consider p be R_eal, q be Real such that

       A2: I = ].p, q.];

      consider r be R_eal, s be Real such that

       A3: J = ].r, s.] by A1;



       A4: (I /\ J) = ].( max (p,r)), ( min (q,s)).] by A2, A3, XXREAL_1: 141;

      ( max (p,r)) is R_eal & ( min (q,s)) is Real by XXREAL_0:def 1;

      then (I /\ J) is left_open_interval by A4;

      hence (I /\ J) is Interval;

    end;

    theorem :: SRINGS_3:27

    for S be Subset-Family of REAL st S = { I where I be Subset of REAL : I is right_open_interval } holds S is with_empty_element semi-diff-closed cap-closed

    proof

      let S be Subset-Family of REAL ;

      assume

       A1: S = { I where I be Subset of REAL : I is right_open_interval };

       0 in REAL by NUMBERS: 19;

      then [. 0 , 0 .[ is right_open_interval by NUMBERS: 31;

      then {} in S by A1;

      hence S is with_empty_element;

      now

        let A,B be set;

        assume

         A2: A in S & B in S;

        then

        consider I be Subset of REAL such that

         A3: A = I & I is right_open_interval by A1;

        consider J be Subset of REAL such that

         A4: B = J & J is right_open_interval by A1, A2;

        per cases ;

          suppose I meets J;

          then

          consider K,L be Subset of REAL such that

           A5: K is right_open_interval & L is right_open_interval & K misses L & (I \ J) = (K \/ L) by A3, A4, INTERVAL02;

          set F = <*K, L*>;

          K in S & L in S by A1, A5;

          then {K, L} c= S by ZFMISC_1: 32;

          then ( rng F) c= S by FINSEQ_2: 127;

          then

          reconsider F as FinSequence of S by FINSEQ_1:def 4;

          reconsider F as disjoint_valued FinSequence of S by A5, Disjoint2;

          take F;

          ( rng F) = {K, L} by FINSEQ_2: 127;

          hence ( Union F) = (A \ B) by A3, A4, A5, ZFMISC_1: 75;

        end;

          suppose

           A13: I misses J;

          set F = <*I*>;

           {I} c= S by A2, A3, ZFMISC_1: 31;

          then ( dom F) = ( Seg 1) & ( rng F) c= S by FINSEQ_1: 38;

          then

          reconsider F as FinSequence of S by FINSEQ_1:def 4;

          reconsider F as disjoint_valued FinSequence of S by TTT1;

          take F;

          ( rng F) = {I} by FINSEQ_1: 38;

          hence ( Union F) = (A \ B) by A13, A3, A4, XBOOLE_1: 83;

        end;

      end;

      hence S is semi-diff-closed;

      now

        let A,B be set;

        assume

         B2: A in S & B in S;

        then

        consider I be Subset of REAL such that

         B3: A = I & I is right_open_interval by A1;

        consider J be Subset of REAL such that

         B4: B = J & J is right_open_interval by A1, B2;

        (I /\ J) is right_open_interval by B3, B4, INTERVAL03;

        hence (A /\ B) in S by A1, B3, B4;

      end;

      hence S is cap-closed;

    end;

    theorem :: SRINGS_3:28

     the set of all I where I be Interval is semialgebra_of_sets of REAL

    proof

      set S = the set of all I where I be Interval;

      now

        let A be object;

        assume A in S;

        then

        consider I be Interval such that

         A2: A = I;

        thus A in ( bool REAL ) by A2;

      end;

      then S c= ( bool REAL );

      then

      reconsider S as Subset-Family of REAL ;

       {} c= REAL ;

      then

      reconsider E = {} as Subset of REAL ;



       A3: E in S;

      then

       A4: S is with_empty_element;

      now

        let A,B be set;

        assume

         A5: A in S & B in S;

        then

        consider I be Interval such that

         A6: A = I;

        consider J be Interval such that

         A7: B = J by A5;

        per cases ;

          suppose

           A8: I misses J;

          set F = <*A*>;



           A9: ( rng F) = {A} by FINSEQ_1: 38;

          then

          reconsider F as FinSequence of S by A5, ZFMISC_1: 31, FINSEQ_1:def 4;

          reconsider F as disjoint_valued FinSequence of S by TTT1;

          take F;

          thus ( Union F) = (A \ B) by A6, A8, A7, XBOOLE_1: 83, A9;

        end;

          suppose

           A10: I meets J;

          (I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval) & (J is open_interval or J is closed_interval or J is right_open_interval or J is left_open_interval) by MEASURE5: 1;

          then

          consider K,L be Interval such that

           A11: K misses L & (I \ J) = (K \/ L) by A10, OOdif, OCdif, ORdif, OLdif, COdif, CCdif, CRdif, CLdif, ROdif, RCdif, RRdif, RLdif, LOdif, LCdif, LRdif, LLdif;

          set F = <*K, L*>;

          K in S & L in S;

          then {K, L} c= S by ZFMISC_1: 32;

          then ( rng F) c= S by FINSEQ_2: 127;

          then

          reconsider F as FinSequence of S by FINSEQ_1:def 4;

          reconsider F as disjoint_valued FinSequence of S by A11, Disjoint2;

          take F;

          ( rng F) = {K, L} by FINSEQ_2: 127;

          hence ( Union F) = (A \ B) by A6, A7, A11, ZFMISC_1: 75;

        end;

      end;

      then

       P2: S is semi-diff-closed;

      now

        let A,B be set;

        assume

         A12: A in S & B in S;

        then

        consider I be Interval such that

         A13: A = I;

        consider J be Interval such that

         A14: B = J by A12;

        per cases ;

          suppose I misses J;

          hence (A /\ B) in S by A3, A13, A14;

        end;

          suppose

           A15: I meets J;

          (I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval) & (J is open_interval or J is closed_interval or J is right_open_interval or J is left_open_interval) by MEASURE5: 1;

          then (I /\ J) is Interval by A15, OOmeet, OCmeet, ORmeet, OLmeet, CCmeet, CRmeet, CLmeet, RRmeet, RLmeet, LLmeet;

          hence (A /\ B) in S by A13, A14;

        end;

      end;

      then

       P3: S is cap-closed;

      reconsider R = ]. -infty , +infty .[ as Subset of REAL ;

      R is open_interval;

      then REAL in S by XXREAL_1: 224;

      hence thesis by A4, P2, P3, Def1;

    end;