:: Semiring of Sets: Examples
::  by Roland Coghetto
:: 
:: Received March 31, 2014
:: Copyright (c) 2014-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies CARD_1, CARD_3, EQREL_1, FINSET_1, FINSUB_1, FUNCT_1, MCART_1,
      NUMBERS, PROB_1, RELAT_1, SETFAM_1, SIMPLEX0, SRINGS_1, SUBSET_1, TARSKI,
      XBOOLE_0, ZFMISC_1, ARYTM_1, ARYTM_3, COMPLEX1, MEASURE5, ORDINAL1,
      REAL_1, SUPINF_1, XREAL_0, XXREAL_0, XXREAL_1, SRINGS_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, SETFAM_1, FINSET_1,
      CARD_1, CARD_3, RELAT_1, FINSUB_1, PROB_1, FUNCT_1, SIMPLEX0, XTUPLE_0,
      WELLORD2, MCART_1, SRINGS_1, ORDINAL1, COMPLEX1, NUMBERS, XXREAL_0,
      XREAL_0, XXREAL_1, XXREAL_3, MEASURE5, RCOMP_1, SUPINF_1, ENUMSET1;
 constructors SRINGS_1, TOPGEN_4, COMPLEX1, RELSET_1, SIMPLEX0, FINSUB_1,
      SUPINF_1, RCOMP_1, MEASURE5, TOPGEN_3, ARYTM_2, ENUMSET1, PARTIT1;
 registrations CARD_1, CARD_3, EQREL_1, FINSET_1, FINSUB_1, MEASURE1, PROB_1,
      SIMPLEX0, SRINGS_1, SUBSET_1, XBOOLE_0, XTUPLE_0, ZFMISC_1, SETFAM_1,
      MEMBERED, NAT_1, RELSET_1, XREAL_0, XXREAL_0, XXREAL_1, XXREAL_3;
 requirements BOOLE, SUBSET, ARITHM, NUMERALS, REAL;
 definitions FINSUB_1, FUNCT_1, SRINGS_1, TARSKI, XBOOLE_0;
 equalities CARD_3, RCOMP_1, XXREAL_0, XXREAL_1;
 expansions TARSKI, XBOOLE_0;
 theorems CARD_1, CARD_3, CARD_4, DILWORTH, EQREL_1, FINSUB_1, LATTICE5,
      PARTIT1, PROB_1, PUA2MSS1, SETFAM_1, SRINGS_1, SUBSET_1, TARSKI,
      XBOOLE_0, XBOOLE_1, XTUPLE_0, YELLOW_8, ZFMISC_1, ABSVALUE, CARD_5,
      FUNCT_1, FUNCT_2, MEASURE5, MESFUNC1, NUMBERS, ORDINAL1, RELSET_1,
      TOPGEN_4, XREAL_0, XREAL_1, XXREAL_0, XXREAL_1, ENUMSET1;
 schemes FUNCT_1, XBOOLE_0;

begin :: Preliminaries

 reserve X for set;
 reserve S for Subset-Family of X;

theorem
  for X1,X2 be set, S1 be Subset-Family of X1, S2 be Subset-Family of X2
  holds {[:a,b:] where a is Element of S1, b is Element of S2:a in S1 &
  b in S2} = {s where s is Subset of [:X1,X2:] : ex a,b be set st a in S1 &
  b in S2 & s=[:a,b:]}
  proof
    let X1,X2 be set;
    let S1 be Subset-Family of X1;
    let S2 be Subset-Family of X2;
    thus {[:a,b:] where a is Element of S1, b is Element of S2:a in S1 &
    b in S2} c= {s where s is Subset of [:X1,X2:] : ex a,b be set st
    a in S1 & b in S2 & s=[:a,b:]}
    proof
      let x be object;
      assume x in {[:a,b:] where a is Element of S1, b is Element of
S2:   a in S1 & b in S2};
      then consider a be Element of S1, b be Element of S2 such that
A1:   x=[:a,b:] & a in S1 & b in S2;
      [:a,b:] c= [:X1,X2:] by A1,ZFMISC_1:96;
      hence thesis by A1;
    end;
    let x be object;
    assume x in {s where s is Subset of [:X1,X2:] : ex a,b be set st
    a in S1 & b in S2 & s=[:a,b:]};
    then ex s0 be Subset of [:X1,X2:] st x=s0 & ex a0,b0 be set st
    a0 in S1 & b0 in S2 & s0=[:a0,b0:];
    hence thesis;
  end;

theorem
  for X1,X2 be set, S1 be non empty Subset-Family of X1,
  S2 be non empty Subset-Family of X2 holds
  {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st x1 in S1 & x2 in S2 &
  s=[:x1,x2:]} =
  the set of all [:x1,x2:] where x1 is Element of S1, x2 is Element of S2
  proof
    let X1,X2 be set;
    let S1 be non empty Subset-Family of X1;
    let S2 be non empty Subset-Family of X2;
A1: for x be object st x in {s where s is Subset of [:X1,X2:]: ex
    x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]} holds x in
    the set of all [:x1,x2:] where x1 is Element of S1, x2 is Element of S2
    proof
      let x be object;
      assume x in {s where s is Subset of [:X1,X2:]: ex
      x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]};
      then ex s be Subset of [:X1,X2:] st
      x=s & ex x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:];
      hence thesis;
    end;
    for x be object st x in the set of all [:x1,x2:] where x1 is Element of S1,
    x2 is Element of S2 holds
    x in {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st
    x1 in S1 & x2 in S2 & s=[:x1,x2:]}
    proof
      let x be object;
      assume x in the set of all [:x1,x2:] where x1 is Element of S1,
      x2 is Element of S2;
      then ex x1 be Element of S1, x2 be Element of S2 st x=[:x1,x2:];
      hence thesis;
    end;
    hence thesis by A1,TARSKI:2;
  end;

theorem
  for X1,X2 be set,S1 be Subset-Family of X1,S2 be Subset-Family of X2 st
  S1 is cap-closed & S2 is cap-closed holds
  {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st x1 in S1 & x2 in S2 &
  s=[:x1,x2:]} is cap-closed
  proof
    let X1,X2 be set, S1 be Subset-Family of X1,
    S2 be Subset-Family of X2;
    assume
A1: S1 is cap-closed;
    assume
A2: S2 is cap-closed;
    set Y= {s where s is Subset of [:X1,X2:]: ex
    x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]};
    Y is cap-closed
    proof
      let W1,W2 be set;
      assume
A3:   W1 in Y;
      assume
A4:   W2 in Y;
      consider s1 be Subset of [:X1,X2:] such that
A5:   W1=s1 & ex xs1,xs2 be set st xs1 in S1 & xs2 in S2 &
      s1=[:xs1,xs2:] by A3;
      consider xs1,xs2 be set such that
A6:   xs1 in S1 & xs2 in S2 & s1=[:xs1,xs2:] by A5;
      consider s2 be Subset of [:X1,X2:] such that
A7:   W2=s2 & ex ys1,ys2 be set st ys1 in S1 & ys2 in S2 &
      s2=[:ys1,ys2:] by A4;
      consider ys1,ys2 be set such that
A8:   ys1 in S1 & ys2 in S2 & s2=[:ys1,ys2:] by A7;
A9:   [:xs1,xs2:]/\[:ys1,ys2:]=[:xs1/\ys1,xs2/\ys2:] by ZFMISC_1:100;
A10:  xs1/\ys1 in S1 & xs2/\ys2 in S2 by A6,A8,A1,A2,FINSUB_1:def 2;
      s1/\s2 in Y by A6,A8,A9,A10;
      hence thesis by A5,A7;
    end;
    hence thesis;
  end;

Lem3:
  for X1,X2 be set,
  S1 be Subset-Family of X1,
  S2 be Subset-Family of X2 holds
  {s where s is Subset of [:X1,X2:]: ex s1,s2 be set st s1 in S1 & s2 in S2 &
  s=[:s1,s2:]} is Subset-Family of [:X1,X2:]
  proof
    let X1,X2 be set;
    let S1 be Subset-Family of X1;
    let S2 be Subset-Family of X2;
    set S = {s where s is Subset of [:X1,X2:]:
    ex s1,s2 be set st s1 in S1 & s2 in S2 & s=[:s1,s2:]};
    S c= bool [:X1,X2:]
    proof
      let x be object;
      assume x in S;
      then consider s0 be Subset of [:X1,X2:] such that
A1:   x=s0 & ex s1,s2 be set st s1 in S1 & s2 in S2 & s0=[:s1,s2:];
      thus thesis by A1;
    end;
    hence thesis;
  end;

Lem4:
  for X1,X2,Y1,Y2 be set holds
  [:X1,X2:]\[:Y1,Y2:]= [:X1\Y1,X2:]\/[:X1/\Y1,X2\Y2:] &
  [:X1\Y1,X2:] misses [:X1/\Y1,X2\Y2:]
  proof
    let X1,X2,Y1,Y2 be set;
A2: [:X1\Y1,X2:]\/[:X1,X2\Y2:] c= [:X1\Y1,X2:]\/[:X1/\Y1,X2\Y2:]
    proof
      let x be object;
      assume
A3:   x in [:X1\Y1,X2:]\/[:X1,X2\Y2:];
      now
        per cases by A3,XBOOLE_0:def 3;
        suppose x in [:X1\Y1,X2:];
          hence thesis by XBOOLE_0:def 3;
        end;
        suppose x in [:X1,X2\Y2:];
          then consider x1,x2 be object such that
A4:       x1 in X1 and
A5:       x2 in X2\Y2 and
A6:       x=[x1,x2] by ZFMISC_1:def 2;
          (x1 in X1 & not x1 in Y1) or
          (x1 in X1 & x1 in Y1) by A4;
          then (x1 in (X1\Y1) & x2 in X2) or (x1 in (X1/\Y1)&
          x2 in X2\Y2) by A5,XBOOLE_0:def 4,def 5;
          then x in [:X1\Y1,X2:] or x in [:X1/\Y1,X2\Y2:]
          by A6,ZFMISC_1:def 2;
          hence thesis by XBOOLE_0:def 3;
        end;
      end;
      hence thesis;
    end;
A7:   [:X1\Y1,X2:]\/[:X1/\Y1,X2\Y2:] c= [:X1\Y1,X2:]\/[:X1,X2\Y2:]
    proof
      let x be object;
      assume
A8:   x in [:X1\Y1,X2:]\/[:X1/\Y1,X2\Y2:];
      now
        per cases by A8,XBOOLE_0:def 3;
        suppose x in [:X1\Y1,X2:];
          hence thesis by XBOOLE_0:def 3;
        end;
        suppose x in [:X1/\Y1,X2\Y2:];
          then consider x1,x2 be object such that
A9:       x1 in X1/\Y1 and
A10:      x2 in X2\Y2 and
A11:      x=[x1,x2] by ZFMISC_1:def 2;
          x1 in X1 & x2 in X2\Y2 & x=[x1,x2]
          by A9,A10,A11,XBOOLE_0:def 4;
          then x in [:X1,X2\Y2:] by ZFMISC_1:def 2;
          hence thesis by XBOOLE_0:def 3;
        end;
      end;
      hence thesis;
    end;
    [:X1\Y1,X2:] misses [:X1/\Y1,X2\Y2:]
    proof
      now
        let x be object;
        assume x in [:X1\Y1,X2:] /\ [:X1/\Y1,X2\Y2:];
        then
A12:    x in [:X1\Y1,X2:] & x in [:X1/\Y1,X2\Y2:] by XBOOLE_0:def 4;
        then consider a1,a2 be object such that
A13:    a1 in X1\Y1 & a2 in X2 & x=[a1,a2] by ZFMISC_1:def 2;
        consider a3,a4 be object such that
A14:    a3 in X1/\Y1 & a4 in X2\Y2 & x=[a3,a4] by ZFMISC_1:def 2,A12;
        a1=a3 & a2=a4 by XTUPLE_0:1,A13,A14;
        then a1 in X1 & not a1 in Y1 & a1 in Y1 by A13,A14,XBOOLE_0:def 4,
        XBOOLE_0:def 5;
        hence contradiction;
      end;
      then [:X1\Y1,X2:] /\ [:X1/\Y1,X2\Y2:] is empty;
      hence thesis;
    end;
    hence thesis by A2,A7,ZFMISC_1:103;
  end;

Lem6a:
  for X be set, S be Subset-Family of X, XX be Subset of S holds union XX=X
  iff XX is Cover of X
  proof
    let X be set, S be Subset-Family of X, XX be Subset of S;
    XX is Subset-Family of X by XBOOLE_1:1;
    hence thesis by SETFAM_1:45;
  end;

registration
  let X be set;
  cluster -> cap-finite-partition-closed diff-c=-finite-partition-closed
  with_countable_Cover with_empty_element for SigmaField of X;
  coherence
  proof
    let SF be SigmaField of X;
    set U={X};
A1: U is Subset-Family of X by ZFMISC_1:68;
A2: union U=X;
    X is Element of SF by PROB_1:5;
    then U is Subset of SF by SUBSET_1:33;
    hence thesis by A1,SETFAM_1:45,def 8,A2,SRINGS_1:def 4,PROB_1:4;
  end;
end;

begin :: Ordinary Examples of Semirings of Sets

theorem
  for F being SigmaField of X holds F is semiring_of_sets of X;

registration
  let X be set;
  cluster bool X -> cap-finite-partition-closed diff-c=-finite-partition-closed
  with_countable_Cover with_empty_element for Subset-Family of X;
  coherence;
end;

theorem
  bool X is semiring_of_sets of X;

Lemme4:
  for X be set, a,b,c be object st [a,b] in [:X,bool X:] & c in X &
  [a,b]=[c,{c}] holds a=c & b={c}
  proof
    let X be set, a,b,c be object;
    assume [a,b] in [:X,bool X:];
    assume c in X;
    assume
A1: [a,b]=[c,{c}];
    [a,b]`1=a & [a,b]`2=b & [c,{c}]`1=c & [c,{c}]`2={c};
    hence thesis by A1;
  end;

FinConv:
  for D be set, SD be Subset-Family of D holds SD={y where y is Subset of D :
  y is finite} iff SD=Fin D
  proof
    let D be set, SD be Subset-Family of D;
    thus SD={y where y is Subset of D : y is finite} implies SD=Fin D
    proof
      assume
A1:   SD={y where y is Subset of D : y is finite};
      thus SD c= Fin D
      proof
        let x be object;
        assume x in SD;
        then ex y be Subset of D st x=y & y is finite by A1;
        hence thesis by FINSUB_1:def 5;
      end;
      let x be object;
      assume
B1:   x in Fin D;
      reconsider x as set by TARSKI:1;
      x c= D & x is finite by B1,FINSUB_1:def 5;
      hence thesis by A1;
    end;
    for D be set, SD be Subset-Family of D st SD=Fin D holds
    SD={y where y is Subset of D : y is finite}
    proof
      let D be set;
      let SD be Subset-Family of D;
      assume
A4:   SD=Fin D;
      then
A5:   SD c= {y where y is Subset of D : y is finite};
      {y where y is Subset of D : y is finite} c= SD
      proof
        let x be object;
        assume x in {y where y is Subset of D : y is finite};
        then consider y be Subset of D such that
A6:     x=y & y is finite;
        thus thesis by A4,A6,FINSUB_1:def 5;
      end;
      hence thesis by A5;
    end;
    hence thesis;
  end;

registration
  let X;
  cluster Fin X -> cap-finite-partition-closed
  diff-c=-finite-partition-closed with_empty_element for Subset-Family of X;
  coherence
  proof
    Fin X is cap-closed
    proof
      let x,y be set;
      assume x in Fin X & y in Fin X;
      then
A2:   x is finite & y is finite & x c= X & y c= X by FINSUB_1:def 5;
      x/\y c= x by XBOOLE_1:17;
      then x/\y is finite & x/\y c= X by A2;
      hence thesis by FINSUB_1:def 5;
    end;
    hence thesis by FINSUB_1:7,SETFAM_1:def 8;
  end;
end;

registration
  let D be denumerable set;
  cluster Fin D -> with_countable_Cover for Subset-Family of D;
  coherence
  proof
    let SD be Subset-Family of D;
    assume SD=Fin D;
    then
A1: SD={y where y is Subset of D : y is finite} by FinConv;
    defpred P[object] means $1 in SD & ex x be set st x in D & $1={x};
    consider XX being set such that
A2: for y being object holds
    y in XX iff y in bool D & P[y] from XBOOLE_0:sch 1;
    for x being object holds x in XX implies x in SD by A2;
    then
A3: XX is Subset of SD by TARSKI:def 3;
A4: for x be object holds x in union XX iff x in D
    proof
      let x be object;
      thus x in union XX implies x in D
      proof
        assume
A5:     x in union XX;
        consider U be set such that
A6:     x in U & U in XX by A5,TARSKI:def 4;
        consider y0 be set such that
A7:     y0 in D & U={y0} by A2,A6;
        thus x in D by A6,A7,TARSKI:def 1;
      end;
      thus thesis
      proof
        assume
A8:     x in D;
        then
A9:     {x} is Subset of D by SUBSET_1:41;
A10:    {x} in SD by A1,A9;
        set y={x};
        x in y & y in XX by A2,A8,A10,TARSKI:def 1;
        hence x in union XX by TARSKI:def 4;
      end;
    end;
A11: union XX = D by A4,TARSKI:2;
    XX is countable
    proof
      D,XX are_equipotent
      proof
        defpred P[object] means ex x be set st x in D & $1=[x,{x}];
        consider Z being set such that
A12:    for z being object holds
        z in Z iff z in [:D,bool D:] & P[z] from XBOOLE_0:sch 1;
        (for c be object st c in D ex xx be object st xx in XX & [c,xx] in Z)&
        (for xx be object st xx in XX ex c be object st c in D & [c,xx] in Z)&
        (for w1,w2,w3,w4 be object st [w1,w2] in Z &
        [w3,w4] in Z holds w1=w3 iff w2=w4)
        proof
A13:      for c be object st c in D ex xx be object st xx in XX & [c,xx] in Z
          proof
            let c be object;
            assume
A14:        c in D;
            set xx0={c};
            take xx0;
            [c,xx0] in [:D,bool D:] & xx0 in XX & [c,xx0] in Z
            proof
A15:          {c} is Subset of D by A14,SUBSET_1:33;
A16:          xx0 in SD by A1,A15;
A17:          {c} c= D by A14,ZFMISC_1:31;
              [c,{c}] in [:D,bool D:] by A14,A17,ZFMISC_1:def 2;
              hence thesis by A2,A12,A14,A16;
            end;
            hence thesis;
          end;
A19:      for xx be object st xx in XX ex c be object st c in D & [c,xx] in Z
          proof
            let xx be object;
            assume
A20:        xx in XX;
            consider c0 be set such that
A21:        c0 in D & xx={c0} by A2,A20;
            take c0;
            [c0,xx] in [:D,bool D:] & [c0,xx] in Z
            proof
              [c0,{c0}] in [:D,bool D:]
              proof
                {c0} is Subset of D by A21,SUBSET_1:41;
                hence thesis by A21,ZFMISC_1:def 2;
              end;
              hence thesis by A12,A21;
            end;
            hence thesis by A21;
          end;
          (for w1,w2,w3,w4 be object st [w1,w2] in Z &
          [w3,w4] in Z holds w1=w3 iff w2=w4)
          proof
            let w1,w2,w3,w4 be object;
            assume
A23:        [w1,w2] in Z;
            assume
A24:        [w3,w4] in Z;
            thus w1=w3 implies w2=w4
            proof
              assume
A25:          w1=w3;
A26:          [w1,w2] in [:D,bool D:] &
              ex x0 be set st x0 in D & [w1,w2]=[x0,{x0}] by A12,A23;
              consider x0 be set such that
A27:          x0 in D & [w1,w2]=[x0,{x0}] by A12,A23;
A28:          w1=x0 & w2={x0} by A26,A27,Lemme4;
A29:          [w1,w4] in [:D,bool D:] &
              ex y0 be set st y0 in D & [w1,w4]=[y0,{y0}] by A12,A24,A25;
              consider y0 be set such that
A30:          y0 in D & [w1,w4]=[y0,{y0}] by A12,A24,A25;
A31:          w1=y0 & w4={y0} by A29,A30,Lemme4;
              thus thesis by A28,A31;
            end;
            thus w2=w4 implies w1=w3
            proof
              assume
A32:          w2=w4;
A33:          [w1,w2] in [:D,bool D:] &
              ex x0 be set st x0 in D & [w1,w2]=[x0,{x0}] by A12,A23;
              consider x0 be set such that
A34:          x0 in D & [w1,w2]=[x0,{x0}] by A12,A23;
A35:          w1=x0 & w2={x0} by A33,A34,Lemme4;
A36:          [w3,w2] in [:D,bool D:] &
              ex y0 be set st y0 in D & [w3,w2]=[y0,{y0}] by A12,A24,A32;
              consider y0 be set such that
A37:          y0 in D & [w3,w2]=[y0,{y0}] by A12,A24,A32;
              w3=y0 & w2={y0} by A36,A37,Lemme4;
              hence thesis by A35,ZFMISC_1:3;
            end;
          end;
          hence thesis by A13,A19;
        end;
        hence thesis;
      end;
      hence thesis by YELLOW_8:4;
    end;
    hence thesis by A3,A11,Lem6a,SRINGS_1:def 4;
  end;
end;

theorem
  Fin X is semiring_of_sets of X
  proof
    Fin X c= bool X by FINSUB_1:13;
    then Fin X is Subset-Family of X;
    hence thesis;
  end;

Lemme9:
  for X1,X2 be non empty set,S1 be non empty Subset-Family of X1,
  S2 be non empty Subset-Family of X2 holds {[:a,b:] where a is Element
  of S1, b is Element of S2:a in S1\{{}} & b in S2\{{}}}= {s where s is
  Subset of [:X1,X2:] : ex a,b be set st a in (S1\{{}}) & b in (S2\{{}}) &
  s=[:a,b:]}
  proof
    let X1,X2 be non empty set;
    let S1 be non empty Subset-Family of X1;
    let S2 be non empty Subset-Family of X2;
    thus {[:a,b:] where a is Element of S1, b is Element of S2:a in S1\{{}} &
    b in S2\{{}}} c= {s where s is Subset of [:X1,X2:] : ex a,b be set st
    a in S1\{{}} & b in S2\{{}} & s=[:a,b:]}
    proof
      let x be object;
      assume x in {[:a,b:] where a is Element of S1, b is Element of
      S2:a in S1\{{}} & b in S2\{{}}};
      then consider a be Element of S1, b be Element of S2 such that
A1:   x=[:a,b:] & a in S1\{{}} & b in S2\{{}};
      thus thesis by A1;
    end;
    let x be object;
    assume x in  {s where s is Subset of [:X1,X2:] : ex a,b be set st
    a in S1\{{}} & b in S2\{{}} & s=[:a,b:]};
    then consider s0 be Subset of [:X1,X2:] such that
A2: x=s0 & ex a0,b0 be set st
    a0 in S1\{{}} & b0 in S2\{{}} & s0=[:a0,b0:];
    consider a0,b0 be set such that
A3: a0 in S1\{{}} & b0 in S2\{{}} & s0=[:a0,b0:] by A2;
    a0 in S1 & b0 in S2 & s0=[:a0,b0:] by TARSKI:def 3,A3,XBOOLE_1:36;
    hence thesis by A2,A3;
  end;

Lem7:
  for x,S1,S2 be set holds
  x in {[:a,b:] where a is Element of (S1\{{}}),
  b is Element of (S2\{{}}):a in S1\{{}} &
  b in S2\{{}}} iff x in
  {[:a,b:] where a is Element of S1, b is Element of S2:a in S1\{{}} &
  b in S2\{{}}}
  proof
    let x, S1,S2 be set;
    x in {[:a,b:] where a is Element of (S1\{{}}),
    b is Element of (S2\{{}}):a in S1\{{}} &
    b in S2\{{}}} iff ex a0 be Element of S1\{{}}, b0 be Element of S2\{{}}
    st x=[:a0,b0:] & a0 in S1\{{}} & b0 in S2\{{}};
    then x in {[:a,b:] where a is Element of (S1\{{}}),
    b is Element of (S2\{{}}):a in S1\{{}} &
    b in S2\{{}}} iff ex a0 be Element of S1, b0 be Element of S2
    st x=[:a0,b0:] & a0 in S1\{{}} & b0 in S2\{{}};
    hence thesis;
  end;

Lem8:
  for X1,X2 be non empty set, S1 be non empty Subset-Family of X1,S2 be
  non empty Subset-Family of X2 holds  {[:a,b:] where a is Element of
  S1\{{}}, b is Element of S2\{{}}: a in S1\{{}} & b in S2\{{}}} =
  {[:a,b:] where a is Element of S1, b is Element of S2:a in S1\{{}} &
  b in S2\{{}}}
  proof
    let X1,X2 be non empty set;
    let S1 be non empty Subset-Family of X1;
    let S2 be non empty Subset-Family of X2;
    for x0 be object holds
    x0 in {[:a,b:] where a is Element of S1\{{}},
    b is Element of S2\{{}}:a in S1\{{}} &
    b in S2\{{}}} iff
    x0 in {[:a,b:] where a is Element of S1,
    b is Element of S2:a in S1\{{}} &
    b in S2\{{}}} by Lem7;
    hence thesis by TARSKI:2;
  end;

Lem9:
  for X be set, S be Subset-Family of X, A be Subset of S holds
  A is Subset-Family of X
  proof
    let X be set;
    let S be Subset-Family of X;
    let A be Subset of S;
    S c= bool X;
    then A c= bool X;
    hence thesis;
  end;

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

theorem
  for X1,X2 be non empty set, S1 be with_countable_Cover Subset-Family of X1,
  S2 be with_countable_Cover Subset-Family of X2, S be Subset-Family of
  [:X1,X2:] st S= {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st
  x1 in S1 & x2 in S2 & s=[:x1,x2:]} holds S is with_countable_Cover
  proof
    let X1,X2 be non empty set;
    let S1 be with_countable_Cover Subset-Family of X1;
    let S2 be with_countable_Cover Subset-Family of X2;
    let S be Subset-Family of [:X1,X2:];
    assume
A1: S= {s where s is Subset of [:X1,X2:]: ex
    x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]};
    ex U be countable Subset of S st union U = [:X1,X2:] & U is Subset of S
    proof
      consider U1 be countable Subset of S1 such that
A2:   U1 is Cover of X1 by SRINGS_1:def 4;
A3:   union U1 = X1 by A2,Lem6a;
      consider U2 be countable Subset of S2 such that
A4:   U2 is Cover of X2 by SRINGS_1:def 4;
A5:   union U2=X2 by A4,Lem6a;
      set U={u where u is Subset of [:X1,X2:] :ex u1,u2 be set st
      u1 in U1\{{}} & u2 in U2\{{}} & u=[:u1,u2:]};
A6:   U1 is non empty by A2,ZFMISC_1:2,Lem6a;
A7:   U1\{{}} is non empty
      proof
        assume U1\{{}} is empty;
        then union U1 c= union {{}} by ZFMISC_1:77,XBOOLE_1:37;
        hence thesis by A2,Lem6a;
      end;
A8:   U2 is non empty by A4,Lem6a,ZFMISC_1:2;
A9:   U2\{{}} is non empty
      proof
        assume U2\{{}} is empty;
        then union U2 c= union {{}} by ZFMISC_1:77,XBOOLE_1:37;
        hence contradiction by A4,Lem6a;
      end;
      set V={[:a,b:] where a is Element of U1,
      b is Element of U2 :a in U1\{{}} & b in U2\{{}}};
A10:  U=V
      proof
        U1 is Subset-Family of X1 & U2 is Subset-Family of X2 by Lem9;
        hence thesis by A6,A8,Lemme9;
      end;
      U is Subset of S
      proof
        for x be object st x in U holds x in S
        proof
          let x be object;
          assume x in U;
          then consider u0 be Subset of [:X1,X2:] such that
A11:      x=u0 & ex u1,u2 be set st
          u1 in U1\{{}} & u2 in U2\{{}} & u0=[:u1,u2:];
          reconsider x as Subset of [:X1,X2:] by A11;
          thus thesis by A1,A11;
        end;
        hence thesis by TARSKI:def 3;
      end;
      then reconsider U as Subset of S;
A12:  U is countable
      proof
        U1\{{}} is countable & U2\{{}} is countable by CARD_3:95;
        then
A13:    [:U1\{{}},U2\{{}}:] is countable by CARD_4:7;
        set W=[:U1\{{}},U2\{{}}:];
        V, W are_equipotent
        proof
          set Z={[[:u1,u2:],[u1,u2]] where u1 is Element of U1,
          u2 is Element of U2: u1 in U1\{{}} & u2 in U2\{{}}};
A14:      (for v be object st v in V ex w be object st w in W & [v,w] in Z)&
          (for w be object st w in W ex v be object st v in V & [v,w] in Z)&
          for v1,v2,w1,w2 be object st [v1,w1] in Z & [v2,w2] in Z holds
          v1=v2 iff w1=w2
          proof
A15:        for v be object st v in V ex w be object st w in W & [v,w] in Z
            proof
              let v be object;
              assume v in V;
              then consider u1 be Element of U1 such that
A16:          ex u2 be Element of U2
              st v=[:u1,u2:] & u1 in U1\{{}} & u2 in U2\{{}};
              consider u2 be Element of U2 such that
A17:          v=[:u1,u2:] & u1 in U1\{{}} & u2 in U2\{{}} by A16;
              set w=[u1,u2];
              take w;
              thus thesis by A17,ZFMISC_1:def 2;
            end;
A18:        for w be object st w in W ex v be object st v in V & [v,w] in Z
            proof
              let w be object;
              assume w in W;
              then ex u1,u2 be object st u1 in U1\{{}} &
              u2 in U2\{{}} & w=[u1,u2] by ZFMISC_1:def 2;
              then consider u1,u2 be set such that
A19:          w=[u1,u2] & u1 in U1\{{}} & u2 in U2\{{}};
              set v=[:u1,u2:];
              take v;
              u1 is Element of U1 & u2 is Element of U2
              by A19,XBOOLE_1:36,TARSKI:def 3;
              hence thesis by A19;
            end;
            for v1,v2,w1,w2 be object st [v1,w1] in Z & [v2,w2] in Z holds
            v1=v2 iff w1=w2
            proof
              let v1,v2,w1,w2 be object;
              assume [v1,w1] in Z;
              then consider a1 be Element of U1, a2 be Element of U2 such that
A21:          [v1,w1]=[[:a1,a2:],[a1,a2]] &
              a1 in U1\{{}} & a2 in U2\{{}};
A22:          v1=[:a1,a2:] & w1=[a1,a2] by A21,XTUPLE_0:1;
              assume [v2,w2] in Z;
              then consider b1 be Element of U1, b2 be Element of U2 such that
A23:          [v2,w2]=[[:b1,b2:],[b1,b2]]&b1 in U1\{{}} & b2 in U2\{{}};
A24:          v2=[:b1,b2:] & w2=[b1,b2] by A23,XTUPLE_0:1;
              thus v1=v2 implies w1=w2
              proof
                assume
A25:            v1=v2;
                not a1 in {{}} & not a2 in {{}} by A21,XBOOLE_0:def 5;
                then a1 <> {} & a2 <>{} by TARSKI:def 1;
                then a1=b1 & a2=b2 by A22,A24,A25,ZFMISC_1:110;
                hence thesis by A21,A23,XTUPLE_0:1;
              end;
              assume
A26:          w1=w2;
              w1=[a1,a2] & w2=[b1,b2] by A21,A23,XTUPLE_0:1;
              then a1=b1 & a2=b2 by A26,XTUPLE_0:1;
              hence thesis by A21,A23,XTUPLE_0:1;
            end;
            hence thesis by A15,A18;
          end;
          ex Z be set st
          (for v be object st v in V ex w be object st w in W & [v,w] in Z)&
          (for w be object st w in W ex v be object st v in V & [v,w] in Z)&
          (for x,y,z,u be object st [x,y] in Z & [z,u] in Z holds
          x=z iff y=u)
          proof
            take Z;
            thus thesis by A14;
          end;
          hence thesis;
        end;
        hence thesis by A10,A13,YELLOW_8:4;
      end;
      union U=[:X1,X2:]
      proof
        set V2= {[:a,b:] where a is Element of U1\{{}},
        b is Element of U2\{{}} : a in U1\{{}} & b in U2\{{}}};
A26:    U=V2
        proof
          U1 is Subset-Family of X1 & U2 is Subset-Family of X2 by Lem9;
          hence thesis by A6,A8,A10,Lem8;
        end;
        union (U1\{{}})=union U1 & union(U2\{{}})=union U2 by PARTIT1:2;
        hence thesis by A3,A5,A7,A9,A26,LATTICE5:2;
      end;
      hence thesis by A12;
    end;
    hence thesis by Lem6a,SRINGS_1:def 4;
  end;

THS0:
  {{}}\/{s where s is Subset of REAL:ex a,b be Real st a<b &
  for x be real number holds x in s iff (a<x & x<=b)} =
  {s where s is Subset of REAL:ex a,b be Real st a<=b &
  for x be real number holds x in s iff (a<x & x<=b)}
  proof
    set S1={{}}\/{s where s is Subset of REAL:ex a,b be Real st a<b &
    for x be real number holds x in s iff (a<x & x<=b)};
    set S2={s where s is Subset of REAL:ex a,b be Real st a<=b &
    for x be real number holds x in s iff (a<x & x<=b)};
A1: S1 c= S2
    proof
      let x be object;
      assume x in S1; then
A2:   x in {{}} or x in {s where s is Subset of REAL:
      ex a,b be Real st a<b &
      for x be real number holds x in s iff (a<x & x<=b)} by XBOOLE_0:def 3;
A3:   x={} implies x in S2
      proof
        set a=0;
        set b=0;
        set s0=].a,b.];
        for x be real number holds x in s0 iff (a<x & x<=b);
        hence thesis;
      end;
      x in {s where s is Subset of REAL:ex a,b be Real st a<b &
      for x be real number holds x in s iff (a<x & x<=b)} implies x in S2
      proof
        assume x in {s where s is Subset of REAL:ex a,b be Real st a<b &
        for t be real number holds t in s iff (a<t & t<=b)};
        then consider s0 be Subset of REAL such that
A4:     s0=x & ex a,b be Real st a<b &
        for t be real number holds t in s0 iff (a<t & t<=b);
        thus thesis by A4;
      end;
      hence thesis by A2,A3,TARSKI:def 1;
    end;
    S2 c= S1
    proof
      let x be object;
      assume x in S2;
      then consider s0 be Subset of REAL such that
A5:   x=s0 and
A6:   ex a,b be Real st a<=b &
      for t be real number holds t in s0 iff (a<t & t<=b);
      consider a,b be Real such that
A7:   a<=b and
A8:   for t be real number holds t in s0 iff (a<t & t<=b) by A6;
A9:   a=b implies x in {{}}
      proof
        assume a=b;
        then s0 c= {} by A8;
        then x={} by A5;
        hence thesis by TARSKI:def 1;
      end;
      a<b implies x in {s where s is Subset of REAL:
      ex a,b be Real st a<b &
      for x be real number holds x in s iff (a<x & x<=b)} by A5,A8;
      hence thesis by XBOOLE_0:def 3,XXREAL_0:1,A7,A9;
    end;
    hence thesis by A1;
  end;

set II = {].a,b.] where a,b is Real:a<=b};
II c= bool REAL
proof
  let x be object;
  assume x in II;
  then ex a0,b0 be Real st x = ].a0,b0.] & a0<=b0;
  hence thesis;
end;
then reconsider II as Subset-Family of REAL;

THS2:
  {s where s is Subset of REAL:ex a,b be Real st a<=b &
  for x be real number holds x in s iff (a<x & x<=b)} = II
  proof
    set S1={s where s is Subset of REAL:ex a,b be Real st a<=b &
    for x be real number holds x in s iff (a<x & x<=b)};
A1: S1 c= II
    proof
      let y be object;
      assume y in S1;
      then consider s0 be Subset of REAL such that
A2:   y=s0 & ex a,b be Real st a<=b &
      for x be real number holds x in s0 iff (a<x & x<=b);
      consider a0,b0 be Real such that
A3:   a0<=b0 & for x be real number holds x in s0 iff (a0<x & x<=b0) by A2;
A4:   s0 c= ].a0,b0.]
      proof
        let x be object;
        assume
A5:     x in s0;
        then reconsider x as real number;
        a0<x & x<=b0 by A3,A5;
        hence thesis;
      end;
      ].a0,b0.] c= s0
      proof
        let x be object;
        assume
A6:     x in ].a0,b0.];
        then reconsider x as real number;
        a0<x & x<=b0 by A6,XXREAL_1:2;
        hence thesis by A3;
      end;
      then s0 = ].a0,b0.] by A4;
      hence thesis by A2,A3;
    end;
    II c= S1
    proof
      let y be object;
      assume y in II;
      then consider a0,b0 be Real such that
A7:   y = ].a0,b0.] & a0<=b0;
      reconsider y as set by TARSKI:1;
      for x be real number holds x in y iff (a0<x & x<=b0) by A7,XXREAL_1:2;
      hence thesis by A7;
    end;
    hence thesis by A1;
  end;

THS1:
  for S be Subset-Family of REAL st
  S={{}}\/{s where s is Subset of REAL:ex a,b be Real st a<b &
  for x be real number holds x in s iff (a<x & x<=b)}
  holds S is cap-closed & S is diff-finite-partition-closed
  with_empty_element Subset-Family of REAL
  proof
    let S be Subset-Family of REAL such that
A1: S={{}}\/{s where s is Subset of REAL:
    ex a,b be Real st a<b &
    for x be real number holds x in s iff (a<x & x<=b)};
A2: S is with_empty_element
    proof
      {} in {{}} by TARSKI:def 1;
      then {} in S by A1,XBOOLE_0:def 3;
      hence thesis;
    end;
A3: S is cap-closed
    proof
      let e1,e2 be set;
      assume
A4:   e1 in S;
      assume
A5:   e2 in S;
A6:   e1 in {{}} or e1 in {s where s is Subset of REAL:
      ex a,b be Real st a<b &
      for x be real number holds x in s iff (a<x & x<=b)}
      by A1,A4,XBOOLE_0:def 3;
A7:   e2 in {{}} or e2 in {s where s is Subset of REAL:
      ex a,b be Real st a<b &
      for x be real number holds x in s iff (a<x & x<=b)}
      by A1,A5,XBOOLE_0:def 3;
A8:   e1={} implies e1/\e2 in S
      proof
        assume e1={};
        then e1/\e2 in {{}} by TARSKI:def 1;
        hence thesis by A1,XBOOLE_0:def 3;
      end;
A9:   e2={} implies e1/\e2 in S
      proof
        assume e2={};
        then e1/\e2 in {{}} by TARSKI:def 1;
        hence thesis by A1,XBOOLE_0:def 3;
      end;
      (e1 in {s where s is Subset of REAL: ex a,b be Real st a<b &
      for x be real number holds x in s iff (a<x & x<=b)}) &
      (e2 in {s where s is Subset of REAL: ex a,b be Real st a<b &
      for x be real number holds x in s iff (a<x & x<=b)}) implies e1/\e2 in S
      proof
        assume
A10:    e1 in {s where s is Subset of REAL:
        ex a,b be Real st a<b &
        for x be real number holds x in s iff (a<x & x<=b)};
        assume
A11:    e2 in {s where s is Subset of REAL:
        ex a,b be Real st a<b &
        for x be real number holds x in s iff (a<x & x<=b)};
        consider E1 be Subset of REAL such that
A12:    e1=E1 & ex a1,b1 be Real st a1<b1 &
        for x be real number holds x in E1 iff (a1<x & x<=b1) by A10;
        consider E2 be Subset of REAL such that
A13:    e2=E2 & ex a2,b2 be Real st a2<b2 &
        for x be real number holds x in E2 iff (a2<x & x<=b2) by A11;
        consider a1,b1 be Real such that
A14:    a1<b1 & for x be real number holds x in E1 iff (a1<x & x<=b1) by A12;
        consider a2,b2 be Real such that
A15:    a2<b2 & for x be real number holds x in E2 iff (a2<x & x<=b2) by A13;
        e1/\e2 in {{}}\/{s where s is Subset of REAL:ex a,b be Real
        st a<b & for x be real number holds x in s iff (a<x & x<=b)}
        proof
A16:    b1<=a2 implies e1/\e2 in {{}}
          proof
            assume
A17:        b1<=a2;
            e1/\e2 c= {}
            proof
              let x be object;
              assume
A18:          x in e1/\e2; then
A19:          x in e1 & x in e2 by XBOOLE_0:def 4;
              reconsider x as real number by A13,A18;
              a1<x & x <= b1 & a2<x & x<=b2 by A12,A13,A14,A15,A19;
              hence thesis by A17,XXREAL_0:2;
            end;
            then e1/\e2={};
            hence thesis by TARSKI:def 1;
          end;
A20:      a2<b1 & a1<b2 implies
          e1/\e2 in {s where s is Subset of REAL:ex a,b be Real st a<b &
          for x be real number holds x in s iff (a<x & x<=b)} or e1/\e2 in {{}}
          proof
            set P={s where s is Subset of REAL:ex a,b be Real st a<b &
            for x be real number holds x in s iff (a<x & x<=b)};
            assume a2<b1 & a1<b2;
A21:        a2<a1 & b2<b1 & a1<b2 implies e1/\e2 in P
            proof
              assume
A22:          a2<a1 & b2<b1;
              assume
A23:          a1<b2;
A24:          for x be real number holds x in e1/\e2 iff (a1<x & x<=b2)
              proof
A25:            for x be real number st x in e1/\e2 holds (a1<x & x<=b2)
                proof
                  let x be real number;
                  assume x in e1/\e2;
                  then x in e1 & x in e2 by XBOOLE_0:def 4;
                  hence thesis by A12,A13,A14,A15;
                end;
                for x be real number st (a1<x & x<=b2) holds x in e1/\e2
                proof
                  let x be real number;
                  assume
A26:              a1<x & x<=b2; then
A27:              x<=b1 by A22,XXREAL_0:2;
                  a1<x & a2<a1 implies a2<x by XXREAL_0:2; then
                  x in e1 & x in e2 by A12,A13,A14,A15,A22,A26,A27;
                  hence thesis by XBOOLE_0:def 4;
                end;
                hence thesis by A25;
              end;
              e1/\e2=E1/\E2 by A12,A13;
              hence thesis by A23,A24;
            end;
A28:        a2<a1 & b2<b1 & not a1<b2 implies e1/\e2 in {{}}
            proof
              assume
A29:          a2<a1 & b2<b1 & not a1<b2;
              e1/\e2 c= {}
              proof
                let x be object;
                assume
A30:            x in e1/\e2; then
A31:            x in e1 & x in e2 by XBOOLE_0:def 4;
                reconsider x as real number by A12,A30;
                a1<x & x <= b1 & a2<x & x<=b2 by A12,A13,A14,A15,A31;
                hence thesis by A29,XXREAL_0:2;
              end;
              then e1/\e2={};
              hence thesis by TARSKI:def 1;
            end;
A32:        a2<a1 & b1<=b2 implies e1/\e2 in P
            proof
              assume
A33:          a2<a1 & b1<=b2;
A34:          for x be real number holds x in e1/\e2 iff (a1<x & x<=b1)
              proof
A35:            for x be real number st x in e1/\e2 holds (a1<x & x<=b1)
                proof
                  let x be real number;
                  assume x in e1/\e2;
                  then x in e1 & x in e2 by XBOOLE_0:def 4;
                  hence thesis by A12,A14;
                end;
                for x be real number st (a1<x & x<=b1) holds x in e1/\e2
                proof
                  let x be real number;
                  assume a1<x & x<=b1;
                  then a1<x & x<=b1 & a2<x & x<=b2 by A33,XXREAL_0:2;
                  then x in e1 & x in e2 by A12,A13,A14,A15;
                  hence thesis by XBOOLE_0:def 4;
                end;
                hence thesis by A35;
              end;
              e1/\e2=E1/\E2 by A12,A13;
              hence thesis by A14,A34;
            end;
A37:        a1<=a2 & b2<b1 implies e1/\e2 in P
            proof
              assume
A38:          a1<=a2 & b2<b1;
A39:          for x be real number holds x in e1/\e2 iff (a2<x & x<=b2)
              proof
A40:            for x be real number st x in e1/\e2 holds (a2<x & x<=b2)
                proof
                  let x be real number;
                  assume x in e1/\e2;
                  then x in e1 & x in e2 by XBOOLE_0:def 4;
                  hence thesis by A13,A15;
                end;
                for x be real number st (a2<x & x<=b2) holds x in e1/\e2
                proof
                  let x be real number;
                  assume
A41:              a2<x & x<=b2;
A42:              a2<x & a1<=a2 implies a1<x by XXREAL_0:2;
                  x<=b2 & b2<b1 implies x<=b1 by XXREAL_0:2;
                  then x in e1 & x in e2 by A12,A13,A14,A15,A38,A41,A42;
                  hence thesis by XBOOLE_0:def 4;
                end;
                hence thesis by A40;
              end;
              e1/\e2=E1/\E2 by A12,A13;
              hence thesis by A15,A39;
            end;
A43:        a1<=a2 & b1<=b2 & not a2<b1 implies e1/\e2 in {{}}
            proof
              assume
A44:          a1<=a2 & b1<=b2 & not a2<b1;
              e1/\e2 c= {}
              proof
                let x be object;
                assume
A45:            x in e1/\e2;
                then
A46:            x in e1 & x in e2 by XBOOLE_0:def 4;
                reconsider x as real number by A12,A45;
                a2<x & x<=b1 by A12,A13,A14,A15,A46;
                hence thesis by A44,XXREAL_0:2;
              end;
              then e1/\e2={};
              hence thesis by TARSKI:def 1;
            end;
            a1<=a2 & b1<=b2 & a2<b1 implies e1/\e2 in P
            proof
              assume
A47:          a1<=a2 & b1<=b2 & a2<b1;
A48:          for x be real number holds x in e1/\e2 iff (a2<x & x<=b1)
              proof
A49:            for x be real number st x in e1/\e2 holds (a2<x & x<=b1)
                proof
                  let x be real number;
                  assume x in e1/\e2;
                  then x in e1 & x in e2 by XBOOLE_0:def 4;
                  hence thesis by A12,A13,A14,A15;
                end;
                for x be real number st (a2<x & x<=b1) holds x in e1/\e2
                proof
                  let x be real number;
                  assume
A50:              a2<x & x<=b1;
                  then
A51:              x<=b2 by A47,XXREAL_0:2;
                  a2<x & a1<=a2 implies a1<x by XXREAL_0:2;
                  then x in e1 & x in e2 by A12,A13,A14,A15,A47,A50,A51;
                  hence thesis by XBOOLE_0:def 4;
                end;
                hence thesis by A49;
              end;
              e1/\e2=E1/\E2 by A12,A13;
              hence thesis by A47,A48;
            end;
            hence thesis by A21,A28,A32,A37,A43;
          end;
          a2<b1 & b2<=a1 implies e1/\e2 in {{}}
          proof
            assume
A52:        a2<b1 & b2<=a1;
            e1/\e2 c= {}
            proof
              let x be object;
              assume
A53:          x in e1/\e2; then
A54:          x in e1 & x in e2 by XBOOLE_0:def 4;
              reconsider x as real number by A12,A53;
              a1<x & x <= b1 & a2<x & x<=b2 by A12,A13,A14,A15,A54;
              hence thesis by A52,XXREAL_0:2;
            end;
            then e1/\e2={};
            hence thesis by TARSKI:def 1;
          end;
          hence thesis by A16,A20,XBOOLE_0:def 3;
        end;
        hence thesis by A1;
      end;
      hence thesis by A6,A7,A8,A9,TARSKI:def 1;
    end;
    S is diff-finite-partition-closed
    proof
      (for S3,S4 be Element of S st S3\S4 is non empty
      ex z be finite Subset of S st
      z is a_partition of S3\S4)
      proof
        let S3,S4 be Element of S;
        assume
A55:    S3\S4 is non empty;
A57:    not S3 in {{}} by A55,TARSKI:def 1;
A58:    S4 in {{}} or S4 in {s where s is Subset of REAL:
        ex a,b be Real st a<b &
        for x be real number holds x in s iff (a<x & x<=b)}
        by A1,XBOOLE_0:def 3;
A59:    S4={} implies ex z be finite Subset of S st
        z is a_partition of S3\S4
        proof
          assume
A60:      S4={};
A61:      {S3} c= S
          proof
            let x be object;
            assume x in {S3};
            then x is Element of S by TARSKI:def 1;
            hence thesis by A2,SUBSET_1:def 1;
          end;
          {S3} is a_partition of S3 by A55,EQREL_1:39;
          hence thesis by A60,A61;
        end;
        S4 in {s where s is Subset of REAL:
        ex a,b be Real st a<b &
        for x be real number holds x in s iff (a<x & x<=b)} implies
        ex z be finite Subset of S st
        z is a_partition of S3\S4
        proof
          assume
A62:      S4 in {s where s is Subset of REAL:
          ex a,b be Real st a<b &
          for x be real number holds x in s iff (a<x & x<=b)};
          S3 in {s where s is Subset of REAL: ex a,b be Real st a<b &
          for x be real number holds x in s iff (a<x & x<=b)}
          by A1,A57,XBOOLE_0:def 3;
          then consider E1 be Subset of REAL such that
A63:      S3=E1 & ex a1,b1 be Real st a1<b1 &
          for x be real number holds x in E1 iff (a1<x & x<=b1);
          consider E2 be Subset of REAL such that
A64:      S4=E2 & ex a2,b2 be Real st a2<b2 &
          for x be real number holds x in E2 iff (a2<x & x<=b2) by A62;
          consider a1,b1 be Real such that
A65:      a1<b1 &
          for x be real number holds x in E1 iff (a1<x & x<=b1) by A63;
          consider a2,b2 be Real such that
A66:      a2<b2 &
          for x be real number holds x in E2 iff (a2<x & x<=b2) by A64;
A67:      for x be real number holds x in S3\S4 iff
          ((a1<x & x<=b1) & not (a2<x & x<=b2))
          proof
A68:        for x be real number st x in S3\S4 holds
            ((a1<x & x<=b1) & not (a2<x & x<=b2) )
            proof
              let x be real number;
              assume x in S3\S4;
              then x in S3 & not x in S4 by XBOOLE_0:def 5;
              hence thesis by A63,A64,A65,A66;
            end;
            for x be real number st
            ((a1<x & x<=b1) & not (a2<x & x<=b2)) holds x in S3\S4
            proof
              let x be real number;
              assume (a1<x & x<=b1) & not (a2<x & x<=b2);
              then x in S3 & not x in S4 by A63,A64,A65,A66;
              hence thesis by XBOOLE_0:def 5;
            end;
            hence thesis by A68;
          end;
A69:      a1<b1 & a2<b2 &b1<= a2 & b1<=b2 implies
          ex z be finite Subset of S st z is a_partition of S3\S4
          proof
            assume
A70:        a1<b1 & a2<b2 &b1<= a2 & b1<=b2;
A71:        S3\S4=S3
            proof
              S3 c= S3\S4
              proof
                let x be object;
                assume
A72:            x in S3;
                then reconsider x as real number by A63;
                a1<x & x<=b1 by A63,A65,A72;
                then ((a1<x & x<=b1) & not (a2<x & x<=b2)) by A70,XXREAL_0:2;
                hence thesis by A67;
              end;
              hence thesis;
            end;
A72a:       {S3} c= S
            proof
              let x be object;
              assume x in {S3};
              then x is Element of S by TARSKI:def 1;
              hence thesis by A2,SUBSET_1:def 1;
            end;
            {S3} is a_partition of S3 by A55,EQREL_1:39;
            hence thesis by A71,A72a;
          end;
A74:      a1<b1 & a2<b2 & a2<b1 & a1<=a2 & b1<=b2 implies
          ex z be finite Subset of S st
          z is a_partition of S3\S4
          proof
            assume
A75:        a1<b1 & a2<b2 & a2<b1 & a1<=a2 & b1<=b2;
A76:        a1<b1 & a2<b2 & a2<b1 & a1=a2 & b1<=b2 implies
            ex z be finite Subset of S st
            z is a_partition of S3\S4
            proof
              assume
A77:          a1<b1 & a2<b2 & a2<b1 & a1=a2 & b1<=b2;
              S3\S4 c= {}
              proof
                let y be object;
                assume
A78:            y in S3\S4;
                then reconsider y as real number by A63;
                (a1<y & y<=b1 ) & (y<=a2 or b2<y) by A67,A78;
                hence thesis by A77,XXREAL_0:2;
              end;
              hence thesis by A55;
            end;
            a1<b1 & a2<b2 & a2<b1 & a1<a2 & b1<=b2 implies
            ex z be finite Subset of S st
            z is a_partition of S3\S4
            proof
              assume
A79:          a1<b1 & a2<b2 & a2<b1 & a1<a2 & b1<=b2;
              set P={x where x is real number:a1<x & x<=a2};
A80:          S3\S4=P
              proof
A81:            S3\S4 c= {x where x is real number:a1<x & x<=a2}
                proof
                  let y be object;
                  assume
A82:              y in S3\S4;
                  then reconsider y as real number by A63;
                  (a1<y & y<=b1) & (y<=a2 or b2<y) by A67,A82;
                  hence thesis by A79,XXREAL_0:2;
                end;
                {x where x is real number:a1<x & x<=a2} c= S3\S4
                proof
                  let y be object;
                  assume y in {x where x is real number:a1<x & x<=a2};
                  then consider y0 be real number such that
A83:              y=y0 & a1<y0 & y0<=a2;
                  (a1<y0 & y0<=b1 ) & (y0<=a2 or b2<y0) by A79,A83,XXREAL_0:2;
                  hence thesis by A67,A83;
              end;
              hence thesis by A81;
            end;
A83a:       {P} c= S
              proof
                let x be object;
                assume x in {P}; then
A84:            x=P by TARSKI:def 1;
                P in {s where s is Subset of REAL:ex a,b be Real
                st a<b & for x be real number holds x in s iff (a<x & x<=b)}
                proof
A86:              P c= REAL
                  proof
                    let x be object;
                    assume x in P;
                    then consider x0 be real number such that
A87:                x=x0 & a1<x0 & x0<=a2;
                    thus thesis by A87,XREAL_0:def 1;
                  end;
                  for x be real number holds x in P iff (a1<x & x<=a2)
                  proof
                    for x be real number st x in P holds (a1<x & x<=a2)
                    proof
                      let x be real number;
                      assume x in P;
                      then consider x0 be real number such that
A89:                  x=x0 & a1<x0 & x0<=a2;
                      thus thesis by A89;
                    end;
                    hence thesis;
                  end;
                  hence thesis by A79,A86;
                end;
                hence thesis by A1,A84,XBOOLE_0:def 3;
              end;
            {P} is a_partition of P by A80,A55,EQREL_1:39;
            hence thesis by A80,A83a;
          end;
          hence thesis by A75,A76,XXREAL_0:1;
        end;
A90:      a1<b1 & a2<b2 & a2<b1 & a1<=a2 & b2<b1 & a1<b2 implies
          ex z be finite Subset of S st
          z is a_partition of S3\S4
          proof
            assume
A91:        a1<b1 & a2<b2 & a2<b1 & a1<=a2 & b2<b1 & a1<b2;
A92:        a1<b1 & a2<b2 & a2<b1 & a1<a2 & b2<b1 & a1<b2 implies
            ex z be finite Subset of S st z is a_partition of S3\S4
            proof
            assume
A93:        a1<b1 & a2<b2 & a2<b1 & a1<a2 & b2<b1 & a1<b2;
            set P1={x where x is Real:a1<x & x<=a2};
A94:        P1 in S
            proof
              P1 in {s where s is Subset of REAL:ex a,b be Real st a<b &
              for x be real number holds x in s iff (a<x & x<=b)}
              proof
                P1 c= REAL
                proof
                  let x be object;
                  assume x in P1;
                  then consider x0 be Real such that
A96:              x=x0 & a1<x0 & x0<=a2;
                  thus thesis by A96,XREAL_0:def 1;
                end; then
A95:            P1 is Subset of REAL;
                for x be real number holds x in P1 iff (a1<x & x<=a2)
                proof
                  for x be real number st x in P1 holds (a1<x & x<=a2)
                  proof
                    let x be real number;
                    assume x in P1;
                    then consider x0 be Real such that
A97:                x=x0 & (a1<x0 & x0<=a2);
                    thus thesis by A97;
                  end;
                  hence thesis;
                end;
                hence thesis by A93,A95;
              end;
              hence thesis by A1,XBOOLE_0:def 3;
            end;
            set P2={x where x is Real:b2<x & x<=b1};
A98:        P2 in S
            proof
              P2 in {s where s is Subset of REAL:ex a,b be Real st a<b &
              for x be real number holds x in s iff (a<x & x<=b)}
              proof
A99:          P2 is Subset of REAL
                proof
                  P2 c= REAL
                  proof
                    let x be object;
                    assume x in P2;
                    then consider x0 be Real such that
A100:               x=x0 & b2<x0 & x0<=b1;
                    thus thesis by A100,XREAL_0:def 1;
                  end;
                  hence thesis;
                end;
                for x be real number holds x in P2 iff (b2<x & x<=b1)
                proof
                  for x be real number st x in P2 holds (b2<x & x<=b1)
                  proof
                    let x be real number;
                    assume x in P2;
                    then consider x0 be Real such that
A101:               x=x0 & (b2<x0 & x0<=b1);
                    thus thesis by A101;
                  end;
                  hence thesis;
                end;
                hence thesis by A93,A99;
              end;
              hence thesis by A1,XBOOLE_0:def 3;
            end;
A101a:      {P1,P2}c=S by A94,A98,TARSKI:def 2;
A102:       {P1,P2} is Subset-Family of S3\S4
            proof
              {P1,P2} c= bool (S3\S4)
              proof
                let x be object;
                assume
A103:           x in {P1,P2};
A104:           P1 in bool (S3\S4)
                proof
                  P1 c= S3\S4
                  proof
                    let x be object;
                    assume x in P1;
                    then consider x0 be Real such that
A105:               x=x0 & a1<x0 & x0<=a2;
                    reconsider x as real number by A105,TARSKI:1;
                    a1<x & x<=a2 & x<=b1 by A93,A105,XXREAL_0:2;
                    hence thesis by A67;
                  end;
                  hence thesis;
                end;
                P2 in bool (S3\S4)
                proof
                  P2 c= S3\S4
                  proof
                    let x be object;
                    assume x in P2;
                    then consider x0 be Real such that
A106:               x=x0 & b2<x0 & x0<=b1;
                    reconsider x as real number by A106,TARSKI:1;
                    a1<x & b2<x & x<=b1 by A93,A106,XXREAL_0:2;
                    hence thesis by A67;
                  end;
                  hence thesis;
                end;
                hence thesis by A103,A104,TARSKI:def 2;
              end;
              hence thesis;
            end;
A107:       union {P1,P2}=S3\S4
            proof
A108:         union{P1,P2}=P1\/P2 by ZFMISC_1:75;
A109:         P1\/P2 c= S3\S4
              proof
                union {P1,P2} c= union (bool (S3\S4)) by A102,ZFMISC_1:77;
                hence thesis by A108,ZFMISC_1:81;
              end;
              S3\S4 c= P1\/P2
              proof
                let y be object;
                assume
A110:           y in S3\S4;
                then reconsider y as real number by A63;
                (a1<y & y<=a2) or
                (b2<y & y<=b1) by A67,A110;
                then y in P1 or y in P2;
                hence thesis by XBOOLE_0:def 3;
              end;
              hence thesis by ZFMISC_1:75,A109;
            end;
            for A be Subset of S3\S4 st A in {P1,P2} holds A<>{} &
            for B be Subset of S3\S4 st B in {P1,P2} holds A=B or A misses B
            proof
              let A be Subset of S3\S4;
              assume
A111:         A in {P1,P2};
A112:         P1 <> {}
              proof
                a2 in P1 by A93;
                hence thesis;
              end;
A113:         P2<>{}
              proof
                b1 in P2 by A93;
                hence thesis;
              end;
              for B be Subset of S3\S4 st B in {P1,P2} holds
              A=B or A misses B
              proof
                let B be Subset of S3\S4;
                assume B in {P1,P2};
                then
A114:           (A=P1 & B=P1) or (A=P1 & B=P2) or (A=P2 & B=P1) or
                (A=P2 & B=P2) by A111,TARSKI:def 2;
                P1 misses P2
                proof
                  P1/\P2 c= {}
                  proof
                    let x be object;
                    assume x in P1/\P2; then
A115:               x in P1 & x in P2 by XBOOLE_0:def 4;
                    then consider x0 be Real such that
A116:               x=x0 & a1<x0 & x0<=a2;
                    consider y0 be Real such that
A117:               x=y0 & b2<y0 & y0<=b1 by A115;
                    thus thesis by A93,A116,A117,XXREAL_0:2;
                  end;
                  hence thesis;
                end;
                hence thesis by A114;
              end;
              hence thesis by A111,A112,A113;
            end;
            then {P1,P2} is a_partition of S3\S4 by A102,A107,EQREL_1:def 4;
            hence thesis by A101a;
          end;
          a1<b1 & a2<b2 & a2<b1 & a1=a2 & b2<b1 & a1<b2 implies
          ex z be finite Subset of S st
          z is a_partition of S3\S4
          proof
            assume
A118:       a1<b1 & a2<b2 & a2<b1 & a1=a2 & b2<b1 & a1<b2;
            set P={x where x is real number:b2<x & x<=b1};
A119:       S3\S4=P
            proof
A120:         S3\S4 c= {x where x is real number:b2<x & x<=b1}
              proof
                let y be object;
                assume
A121:           y in S3\S4;
                then reconsider y as real number by A63;
                (a1<y & y<=b1) & not (a2<y & y<=b2) by A67,A121;
                hence thesis by A118;
              end;
              {x where x is real number:b2<x & x<=b1} c= S3\S4
              proof
                let y be object;
                assume y in {x where x is real number:b2<x & x<=b1};
                then consider y0 be real number such that
A122:           y=y0 & b2<y0 & y0<=b1;
                (a1<y0 & y0<=b1 ) & (y0<=a2 or b2<y0) by A118,A122,XXREAL_0:2;
                hence thesis by A67,A122;
              end;
              hence thesis by A120;
            end;
A123:       {P} c= S
            proof
              let x be object;
              assume x in {P}; then
A124:         x=P by TARSKI:def 1;
              P in {s where s is Subset of REAL:ex a,b be Real st
              a<b & for x be real number holds x in s iff (a<x & x<=b)}
              proof
A125:           P c= REAL
                proof
                  let x be object;
                  assume x in P;
                  then consider x0 be real number such that
A126:             x=x0 & b2<x0 & x0<=b1;
                  thus thesis by A126,XREAL_0:def 1;
                end;
                for x be real number holds x in P iff (b2<x & x<=b1)
                proof
                  for x be real number st x in P holds (b2<x & x<=b1)
                  proof
                    let x be real number;
                    assume x in P;
                    then consider x0 be real number such that
A126a:              x=x0 & b2<x0 & x0<=b1;
                    thus thesis by A126a;
                  end;
                  hence thesis;
                end;
                hence thesis by A118,A125;
              end;
              hence thesis by A1,A124,XBOOLE_0:def 3;
            end;
            {P} is a_partition of P by A55,A119,EQREL_1:39;
            hence thesis by A123,A119;
          end;
          hence thesis by A91,A92,XXREAL_0:1;
        end;
A127:   a1<b1 & a2<b2 & b1<=b2 & a2<b1 & a2<a1 implies
        ex z be finite Subset of S st z is a_partition of S3\S4
        proof
          assume
A128:     a1<b1 & a2<b2 & b1<=b2 & a2<b1 & a2<a1;
          S3\S4 c= {}
          proof
            let y be object;
            assume
A129:       y in S3\S4;
            then reconsider y as real number by A63;
A130:       (a1<y & y<=b1 ) & (y<=a2 or b2<y) by A67,A129;
            thus thesis by A128,A130,XXREAL_0:2;
          end;
          hence thesis by A55;
        end;
A131:   a1<b1 & a2<b2 & b2<b1 & b2<=a1 & a2<b1 & a2<a1 implies
        ex z be finite Subset of S st
        z is a_partition of S3\S4
        proof
          assume
A132:     a1<b1 & a2<b2 & b2<b1 & b2<=a1 & a2<b1 & a2<a1;
          S3 c= S3\S4
          proof
            let x be object;
            assume
A133:       x in S3;
            then reconsider x as real number by A63;
A134:       a1<x & x<=b1 by A63,A65,A133;
            b2<x by A132,A134,XXREAL_0:2;
            hence thesis by A67,A134;
          end;
          then
A135:     S3=S3\S4;
A135a:    {S3} c= S
          proof
            let x be object;
            assume x in {S3};
            then x is Element of S by TARSKI:def 1;
            hence thesis by A2,SUBSET_1:def 1;
          end;
          {S3} is a_partition of S3 by A55,EQREL_1:39;
          hence thesis by A135a,A135;
        end;
        a1<b1 & a2<b2 & (b2<b1 & a1<b2) & a2<b1 & a2<a1 implies
        ex z be finite Subset of S st
        z is a_partition of S3\S4
        proof
          assume
A137:     a1<b1 & a2<b2 & (b2<b1 & a1<b2) & a2<b1 & a2<a1;
          set P={x where x is real number:b2<x & x<=b1};
A138:     S3\S4=P
            proof
A139:         S3\S4 c= {x where x is real number:b2<x & x<=b1}
              proof
                let y be object;
                assume
A140:           y in S3\S4;
                then reconsider y as real number by A63;
                (a1<y & y<=b1&y<=a2) or (a1<y & y<=b1&b2<y) by A67,A140;
                hence thesis by A137,XXREAL_0:2;
              end;
              {x where x is real number:b2<x & x<=b1} c= S3\S4
              proof
                let y be object;
                assume y in {x where x is real number:b2<x & x<=b1};
                then consider y0 be real number such that
A141:           y=y0 & b2<y0 & y0<=b1;
                (a1<y0 & y0<=b1 ) & (y0<=a2 or b2<y0) by A137,A141,XXREAL_0:2;
                hence thesis by A67,A141;
              end;
              hence thesis by A139;
            end;
A142:       {P} c= S
            proof
              let x be object;
              assume x in {P}; then
A143:         x=P by TARSKI:def 1;
              P in {s where s is Subset of REAL: ex a,b be Real st a<b &
              for x be real number holds x in s iff (a<x & x<=b)}
              proof
A144:           P is Subset of REAL
                proof
                  P c= REAL
                  proof
                    let x be object;
                    assume x in P;
                    then consider x0 be real number such that
A145:               x=x0 & b2<x0 & x0<=b1;
                    thus thesis by A145,XREAL_0:def 1;
                  end;
                  hence thesis;
                end;
                for x be real number holds x in P iff (b2<x & x<=b1)
                proof
                  for x be real number st x in P holds (b2<x & x<=b1)
                  proof
                    let x be real number;
                    assume x in P;
                    then consider x0 be real number such that
A146:               x=x0 & b2<x0 & x0<=b1;
                    thus thesis by A146;
                  end;
                  hence thesis;
                end;
                hence thesis by A137,A144;
              end;
              hence thesis by A1,A143,XBOOLE_0:def 3;
            end;
            {P} is a_partition of P by A55,A138,EQREL_1:39;
            hence thesis by A142,A138;
          end;
          hence thesis by A65,A66,A69,A74,A90,A127,A131,XXREAL_0:2;
        end;
        hence thesis by A58,A59,TARSKI:def 1;
      end;
      hence thesis by SRINGS_1:def 2;
    end;
    hence thesis by A2,A3;
  end;

LemmA1:
  II is with_countable_Cover
  proof
    defpred F[object,object] means
    $1 is Element of NAT & $2 in II &
    ex x be real number st x=$1 & $2=].-x,x.];
A2: for x be object st x in NAT holds ex y be object st y in II & F[x,y]
    proof
      let x be object;
      assume
A3:   x in NAT;
      then reconsider x as real number;
      set y = ].-x,x.];
      y in II & F[x,y] by A3;
      hence thesis;
    end;
    consider f be Function such that
A4: dom f=NAT & rng f c= II and
A5: for x be object st x in NAT holds
    F[x,f.x] from FUNCT_1:sch 6(A2);
A6: rng f is Subset-Family of REAL by A4,XBOOLE_1:1;
A7: rng f is countable
    proof
      reconsider f as SetSequence of REAL by A4,A6,RELSET_1:4,FUNCT_2:def 1;
      rng f is countable by TOPGEN_4:58;
      hence thesis;
    end;
    rng f is Cover of REAL
    proof
      Union f=REAL
      proof
        thus Union f c= REAL
        proof
          let x be object;
          assume x in Union f;
          then consider t be object such that
A9:       t in dom f & x in f.t by CARD_5:2;
          consider x0 be real number such that
A10:      x0=t & f.t=].-x0,x0.] by A4,A5,A9;
          thus thesis by A9,A10;
        end;
        let x be object;
        assume x in REAL;
        then reconsider x as Real;
        consider n be Element of NAT such that
A11:    |.x.| <=n by MESFUNC1:8;
A12:    n+1 is Element of NAT by ORDINAL1:def 12;
        x in f.(n+1)
        proof
          consider z be real number such that
A13:      z=(n+1) & f.(n+1)=].-z,z.] by A5,A12;
A14:      -|.x.| <=x & x<=|.x.| & |.x.| <=n by A11,ABSVALUE:4;
A15:      x <= n implies x+0 <= n+1 by XREAL_1:7;
          -(n+1) < x
          proof
            per cases;
            suppose 0<=x;
              hence thesis;
            end;
            suppose x<0;
              then - x <= n by A11,ABSVALUE:def 1; then
A16:          - n <= --x by XREAL_1:24; then
A17:          -n-1 <= x-1 by XREAL_1:13;
              x-1<=x-0 by XREAL_1:13; then
A18:          -(n+1) <= x by A17,XXREAL_0:2;
              -(n+1) < x
              proof
                not -(n+1)=x
                proof
                  assume x=-(n+1);
                  then -n+n<=-(n+1)+n by A16,XREAL_1:7;
                  hence thesis;
                end;
                hence thesis by A18,XXREAL_0:1;
              end;
              hence thesis;
            end;
          end;
          hence thesis by A13,A14,A15,XXREAL_0:2;
        end;
        then x in f.(n+1) & f.(n+1) in rng f by A4,A12,FUNCT_1:def 3;
        hence thesis by TARSKI:def 4;
      end;
      hence thesis by A6,SETFAM_1:45;
    end;
    hence thesis by A4,A7,SRINGS_1:def 4;
  end;

theorem
  for S be Subset-Family of REAL
  st S = {].a,b.] where a,b is Real: a<=b}
  holds S is cap-closed &
  S is diff-finite-partition-closed with_empty_element &
  S is with_countable_Cover by THS0,THS1,THS2,LemmA1;

LemmB:
  for S be Subset-Family of REAL
  st S={s where s is Subset of REAL:s is left_open_interval}
  holds S is with_countable_Cover
  proof
    let S be Subset-Family of REAL;
    assume
A1: S = {s where s is Subset of REAL:s is left_open_interval};
    defpred F[object,object] means
    $1 is Element of NAT & $2 in S &
    ex x be real number st x=$1 & $2=].-infty,x.];
A2: for x be object st x in NAT holds
    ex y be object st y in S & F[x,y]
    proof
      let x be object;
      assume
A3:   x in NAT;
      then reconsider x as real number;
      set y= ].-infty,x.];
A4:   y is Subset of REAL & y is left_open_interval by MEASURE5:def 5;
      F[x,y] by A1,A3,A4;
      hence thesis;
    end;
    consider f be Function such that
A5: dom f=NAT & rng f c= S and
A6: for x be object st x in NAT holds
    F[x,f.x] from FUNCT_1:sch 6(A2);
A7: rng f is Subset-Family of REAL by A5,XBOOLE_1:1;
A8: rng f is countable
    proof
      reconsider f as SetSequence of REAL by A5,A7,RELSET_1:4,FUNCT_2:def 1;
      rng f is countable by TOPGEN_4:58;
      hence thesis;
    end;
    rng f is Cover of REAL
    proof
      union rng f=REAL
      proof
A9:   union rng f c= REAL
        proof
          let x be object;
          assume x in union rng f;
          then x in Union f;
          then consider t be object such that
A10:      t in dom f & x in f.t by CARD_5:2;
          consider x0 be real number such that
A11:      x0=t & f.t=].-infty,x0.] by A5,A6,A10;
          thus thesis by A10,A11;
        end;
        REAL c= union rng f
        proof
          let x be object;
          assume x in REAL;
          then reconsider x as Real;
          consider n be Element of NAT such that
A12:      x<=n by MESFUNC1:8;
          x in f.n
          proof
            ex z be real number st
            z=n & f.n=].-infty,z.] by A6;
            hence thesis by A12,XXREAL_1:234;
          end;
          then x in f.n & f.n in rng f by A5,FUNCT_1:def 3;
          hence thesis by TARSKI:def 4;
        end;
        hence thesis by A9;
      end;
      hence thesis by A7,SETFAM_1:45;
    end;
    hence thesis by A5,A8,SRINGS_1:def 4;
  end;

theorem
  for S be Subset-Family of REAL
  st S = {s where s is Subset of REAL:s is left_open_interval}
  holds S is cap-closed &
  S is diff-finite-partition-closed with_empty_element &
  S is with_countable_Cover
  proof
    let S be Subset-Family of REAL;
    assume
A1: S={s where s is Subset of REAL:s is left_open_interval};
A2: S is cap-closed
    proof
      for S1,S2 being set st S1 in S & S2 in S holds S1/\S2 in S
      proof
        let S1,S2 be set;
        assume
A3:     S1 in S;
        assume
A4:     S2 in S;
        consider s1 be Subset of REAL such that
A5:     S1=s1 & s1 is left_open_interval by A1,A3;
        consider s2 be Subset of REAL such that
A6:     S2=s2 & s2 is left_open_interval by A1,A4;
        set S3=s1/\s2;
        reconsider S3 as Subset of REAL;
        consider a1 being R_eal,b1 being Real such that
A7:     s1=].a1,b1.] by MEASURE5:def 5,A5;
        consider a2 being R_eal,b2 being Real such that
A8:     s2=].a2,b2.] by MEASURE5:def 5,A6;
A9:     S3=].max(a1,a2),min(b1,b2).] by A7,A8,XXREAL_1:141;
        set m1=max(a1,a2);
        m1 in ExtREAL by XXREAL_0:def 1;
        then S3 is left_open_interval by A9,MEASURE5:def 5;
        hence thesis by A1,A5,A6;
      end;
      hence thesis by FINSUB_1:def 2;
    end;
A10: S is with_empty_element
    proof
      ].0,0.] is left_open_interval
      proof
        0 in REAL by NUMBERS:19;
        hence thesis by NUMBERS:31,MEASURE5:def 5;
      end; then
      {} in S by A1;
      hence thesis;
    end;
    then
A12: S is non empty;
    S is diff-finite-partition-closed
    proof
      for S3,S4 be Element of S st S3\S4 is non empty
      ex z be finite Subset of S st
      z is a_partition of S3\S4
      proof
        let S3,S4 be Element of S;
        assume
A13:    S3\S4 is non empty;
A14:    S3 in S & S4 in S by A12;
        consider s3 be Subset of REAL such that
A15:    S3=s3 & s3 is left_open_interval by A1,A14;
        consider s4 be Subset of REAL such that
A16:    S4=s4 & s4 is left_open_interval by A1,A14;
        consider a1 be R_eal,b1 be Real such that
A17:    s3=].a1,b1.] by A15,MEASURE5:def 5;
        consider a2 be R_eal,b2 be Real such that
A18:    s4=].a2,b2.] by A16,MEASURE5:def 5;
A20:    s4 is empty implies
        ex z be finite Subset of S st z is a_partition of S3\S4
        proof
          assume
A21:      s4 is empty;
          set z={S3};
A22:      z c= S by A14,TARSKI:def 1;
          {S3} is a_partition of S3 by A13,EQREL_1:39;
          hence thesis by A22,A16,A21;
        end;
A23:    (s4 is non empty & s3 misses s4) implies
        ex z be finite Subset of S st z is a_partition of S3\S4
        proof
          assume
A24:      s4 is non empty & s3 misses s4;
A25:      S3\S4=S3
          proof
            S3 c= S3\S4
            proof
              let x be object;
              assume
A27:          x in S3;
              not x in S4 by A27,A15,A16,A24,XBOOLE_0:def 4;
              hence thesis by A27,XBOOLE_0:def 5;
            end;
            hence thesis;
          end;
          set z={S3};
A28:      z c= S by A14,TARSKI:def 1;
          z is a_partition of S3 by A13,EQREL_1:39;
          hence thesis by A28,A25;
        end;
        s4 is non empty & s3 meets s4 implies
        ex z be finite Subset of S st z is a_partition of S3\S4
        proof
          assume
A29:      s4 is non empty & s3 meets s4;
          then
A30:      ].a1,b1.] \ ].a2,b2.] = ].a1,a2.] \/ ].b2,b1.]
          by A17,A18,XXREAL_1:199;
A31:      b1<=b2 implies ].a1,a2.] /\ ].b2,b1.] c= {}
          proof
            assume
A32:        b1<=b2;
            ].b2,b1.]={}
            proof
              assume ].b2,b1.]<>{};
              then consider x be object such that
A33:          x in ].b2,b1.] by XBOOLE_0:def 1;
              reconsider x as real number by A33;
              b2<x & x<=b1 by A33,XXREAL_1:2;
              hence thesis by A32,XXREAL_0:2;
            end;
            hence thesis;
          end;
A33a:     b2<b1 implies ].a1,a2.] /\ ].b2,b1.] c= {}
          proof
            assume b2<b1;
            ].a1,a2.] /\ ].b2,b1.] c= {}
            proof
              let x be object;
              assume
A34:          x in ].a1,a2.] /\ ].b2,b1.];
              then
A35:          x in ].a1,a2.] & x in ].b2,b1.] by XBOOLE_0:def 4;
              reconsider x as real number by A34;
              per cases;
              suppose
A36:            a2<=b2;
                b2<x & x<=a2 by A35,XXREAL_1:2;
                hence thesis by A36,XXREAL_0:2;
              end;
              suppose
A37:            b2<a2;
                s4 c= {}
                proof
                  let x be object;
                  assume
A38:              x in s4;
                  then reconsider x as real number;
                  a2<x & x<=b2 by A18,A38,XXREAL_1:2;
                  hence thesis by A37,XXREAL_0:2;
                end;
                hence thesis by A29;
              end;
            end;
            hence thesis;
          end;
A40:      a2 in REAL or a2 in {-infty,+infty} by XBOOLE_0:def 3;
A41:      a2=+infty implies
          ex z be finite Subset of S st
          z is a_partition of S3\S4 by A18,A29,XXREAL_1:216;
A42:      a2= -infty implies
          ex z be finite Subset of S st z is a_partition of S3\S4
          proof
            assume
A43:        a2=-infty;
A44:        S3\S4={}\/].b2,b1.] by A15,A16,A17,A18,A30,A43,XXREAL_1:212;
            set z={].b2,b1.]};
A45:        z c= S
              proof
                let x be object;
                assume
A47:            x in z; then
A48:            x=].b2,b1.] by TARSKI:def 1;
                reconsider x as Subset of REAL by A47,TARSKI:def 1;
                b2 in REAL by XREAL_0:def 1;
                then x is left_open_interval by A48,NUMBERS:31,MEASURE5:def 5;
                hence thesis by A1;
            end;
            z is a_partition of S3\S4 by A44,A13,EQREL_1:39;
            hence thesis by A45;
          end;
A49:      a2 in REAL & not(not(a1<a2) & not(b2<b1)) &
          not(a1<a2 & b2<b1) implies
          ex z be finite Subset of S st z is a_partition of S3\S4
          proof
            assume
A50:        a2 in REAL;
            assume
A51:        not(not(a1<a2) & not(b2<b1)) & not(a1<a2 & b2<b1);
A52:        a1<a2 & b1<=b2 implies
            ex z be finite Subset of S st z is a_partition of S3\S4
            proof
              assume
A53:          a1<a2 & b1<=b2;
              ].b2,b1.] c= {}
              proof
                let x be object;
                assume
A54:            x in ].b2,b1.];
                then reconsider x as real number;
                b2<x & x<=b1 by A54,XXREAL_1:2;
                hence thesis by A53,XXREAL_0:2;
              end; then
A55:          ].b2,b1.]={};
              set z={].a1,a2.]};
A56:          {].a1,a2.]} c= S
                proof
                  let x be object;
                  assume
A57:              x in {].a1,a2.]};
                  ].a1,a2.] in S
                  proof
                    set AA=].a1,a2.];
                    reconsider AA as Subset of REAL by A50,XXREAL_1:227;
                    AA is left_open_interval by A50,MEASURE5:def 5;
                    hence thesis by A1;
                  end;
                  hence thesis by A57,TARSKI:def 1;
                end;
              ].a1,a2.]<>{}
              proof
                a2 in ].a1,a2.] by A53;
                hence thesis;
              end;
              then z is a_partition of ].a1,a2.] by EQREL_1:39;
              hence thesis by A15,A16,A17,A18,A30,A55,A56;
            end;
            b2<b1 & a2<=a1 implies
            ex z be finite Subset of S st z is a_partition of S3\S4
            proof
              assume
A58:          b2<b1 & a2<=a1;
              ].a1,a2.] c= {}
              proof
                let x be object;
                assume
A59:            x in ].a1,a2.];
                then reconsider x as real number by A50;
                a1<x & x<=a2 by A59,XXREAL_1:2;
                hence thesis by A58,XXREAL_0:2;
              end; then
A60:          ].a1,a2.]={};
              set z={].b2,b1.]};
A61:          {].b2,b1.]} c= S
                proof
                  let x be object;
                  assume
A62:              x in {].b2,b1.]};
                  ].b2,b1.] in S
                  proof
                    set AA=].b2,b1.];
                    reconsider AA as Subset of REAL;
                    b2 in REAL by XREAL_0:def 1;
                    then AA is left_open_interval by NUMBERS:31,MEASURE5:def 5;
                    hence thesis by A1;
                  end;
                  hence thesis by A62,TARSKI:def 1;
                end;
              ].b2,b1.]<>{} by A58,XXREAL_1:2;
              then z is a_partition of ].b2,b1.] by EQREL_1:39;
              hence thesis by A15,A16,A17,A18,A30,A60,A61;
            end;
            hence thesis by A51,A52;
          end;
A63:      a2 in REAL & not(a1<a2) & not(b2<b1) implies
          ex z be finite Subset of S st
          z is a_partition of S3\S4
          proof
            assume a2 in REAL;
            assume
A64:        not(a1<a2) & not(b2<b1);
            S3\S4 c= {}
            proof
              let x be object;
              assume
A65:          x in S3\S4; then
A66:          x in ].a1,b1.] & not x in ].a2,b2.]
                by A15,A16,A17,A18,XBOOLE_0:def 5;
              reconsider x as real number by A15,A65;
              a1<x & x<=b1 & (x<=a2 or b2<x) by A66,XXREAL_1:2;
              hence thesis by A64,XXREAL_0:2;
            end;
            hence thesis by A13;
          end;
          a2 in REAL & a1<a2 & b2<b1 implies
          ex z be finite Subset of S st z is a_partition of S3\S4
          proof
            assume
A67:        a2 in REAL;
            assume
            a1<a2 & b2<b1;
            then
A69:        ].a1,a2.] <>{} & ].b2,b1.]<>{} by XXREAL_1:2;
            set z={].a1,a2.], ].b2,b1.]};
A70:        {].a1,a2.], ].b2,b1.]} c= S
              proof
                let x be object;
                assume
A71:            x in {].a1,a2.], ].b2,b1.]};
A72:            ].a1,a2.] in S
                proof
                  set AA=].a1,a2.];
                  reconsider AA as Subset of REAL by A67,XXREAL_1:227;
                  AA is left_open_interval by A67,MEASURE5:def 5;
                  hence thesis by A1;
                end;
                ].b2,b1.] in S
                proof
                  set BB=].b2,b1.];
                  reconsider BB as Subset of REAL;
                  b2 in REAL by XREAL_0:def 1;
                  then BB is left_open_interval by NUMBERS:31,MEASURE5:def 5;
                  hence thesis by A1;
                end;
                hence thesis by A71,A72,TARSKI:def 2;
              end;
            z is a_partition of ].a1,b1.]\].a2,b2.]
            proof
A73:          z is Subset-Family of ].a1,b1.]\].a2,b2.]
              proof
                z c= bool (].a1,b1.]\].a2,b2.])
                proof
                  let x be object;
                  assume x in z;
                  then
A74:              x=].a1,a2.] or x=].b2,b1.] by TARSKI:def 2;
                  reconsider x as set by TARSKI:1;
                  x c= ].a1,b1.]\].a2,b2.]
                  proof
                    let y be object;
                    assume y in x;
                    then y in ].a1,a2.] \/ ].b2,b1.] by A74,XBOOLE_0:def 3;
                    hence thesis by A17,A18,A29,XXREAL_1:199;
                  end;
                  hence thesis;
                end;
                hence thesis;
              end;
A75:          union z = ].a1,b1.]\].a2,b2.] by A30,ZFMISC_1:75;
              for A be Subset of ].a1,b1.]\].a2,b2.] st A in z holds A<>{} &
              for B be Subset of ].a1,b1.]\].a2,b2.] st B in z holds A=B or
              A misses B
              proof
                let A be Subset of ].a1,b1.]\].a2,b2.];
                assume
A76:            A in z;
                for B be Subset of ].a1,b1.]\].a2,b2.] st B in z holds A=B or
                A misses B
                proof
                  let B be Subset of ].a1,b1.]\].a2,b2.];
                  assume B in z;
                  then (A=].a1,a2.] & B=].a1,a2.]) or
                  (A=].a1,a2.] & B=].b2,b1.]) or
                   (A=].b2,b1.] & B=].a1,a2.]) or
                  (A=].b2,b1.] & B=].b2,b1.]) by A76,TARSKI:def 2;
                  hence thesis by A31,A33a;
                end;
                hence thesis by A69,A76;
              end;
              hence thesis by A73,A75,EQREL_1:def 4;
            end;
            hence thesis by A15,A16,A17,A18,A70;
          end;
          hence thesis by A40,A41,A42,A49,A63,TARSKI:def 2;
        end;
        hence thesis by A20,A23;
      end;
      hence thesis by SRINGS_1:def 2;
    end;
    hence thesis by A1,A2,A10,LemmB;
  end;

begin :: Numerical Example

definition
  func sring4_8 -> Subset-Family of {1,2,3,4} equals
  {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}};
  coherence
  proof
    set SF={{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}};
    SF c= bool {1,2,3,4}
    proof
      let x be object;
      assume x in SF;
      then
S1:   x={1,2,3,4} or x={1,2,3} or x={2,3,4} or x={1} or
      x={2} or x={3} or x={4} or x={} by ENUMSET1:def 6;
      reconsider x as set by TARSKI:1;
S3:   {1,2,3} c= {1,2,3,4}
      proof
        let x be object;
        assume x in {1,2,3};
        then x=1 or x=2 or x=3 by ENUMSET1:def 1;
        hence thesis by ENUMSET1:def 2;
      end;
S4:   {2,3,4} c= {1,2,3,4}
      proof
        let x be object;
        assume x in {2,3,4};
        then x=2 or x=3 or x=4 by ENUMSET1:def 1;
        hence thesis by ENUMSET1:def 2;
      end;
S5:   {1} c= {1,2,3,4}
      proof
        let x be object;
        assume x in {1};
        then x=1 by TARSKI:def 1;
        hence thesis by ENUMSET1:def 2;
      end;
S6:   {2} c= {1,2,3,4}
      proof
        let x be object;
        assume x in {2};
        then x=2 by TARSKI:def 1;
        hence thesis by ENUMSET1:def 2;
      end;
S7:   {3} c= {1,2,3,4}
      proof
        let x be object;
        assume x in {3};
        then x=3 by TARSKI:def 1;
        hence thesis by ENUMSET1:def 2;
      end;
S8:   {4} c= {1,2,3,4}
      proof
        let x be object;
        assume x in {4};
        then x=4 by TARSKI:def 1;
        hence thesis by ENUMSET1:def 2;
      end;
      x c= {1,2,3,4} by S1,S3,S4,S5,S6,S7,S8;
      hence thesis;
    end;
    hence thesis;
  end;
end;

set S = sring4_8;

registration
  cluster sring4_8 -> with_empty_element;
  coherence
  proof
    {} in S by ENUMSET1:def 6;
    hence thesis;
  end;
end;

LL2:{1,2,3,4}/\{1,2,3} = {1,2,3}
proof
  now
    let x be object;
    x in {1,2,3,4}/\{1,2,3} iff x in {1,2,3,4} &
    x in {1,2,3} by XBOOLE_0:def 4;
    then x in {1,2,3,4}/\{1,2,3} iff
    x=1 or x=2 or x=3 by ENUMSET1:def 1,ENUMSET1:def 2;
    hence x in {1,2,3,4}/\{1,2,3} iff
    x in {1,2,3} by ENUMSET1:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL3:{1,2,3,4}/\{2,3,4} = {2,3,4}
proof
  now
    let x be object;
    x in {1,2,3,4}/\{2,3,4} iff x in {1,2,3,4} &
    x in {2,3,4} by XBOOLE_0:def 4;
    then x in {1,2,3,4}/\{2,3,4} iff
    x=4 or x=2 or x=3 by ENUMSET1:def 1,ENUMSET1:def 2;
    hence x in {1,2,3,4}/\{2,3,4} iff
    x in {2,3,4} by ENUMSET1:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL4:{1,2,3,4}/\{1} = {1}
proof
  now
    let x be object;
    x in {1,2,3,4}/\{1} iff x in {1,2,3,4} &
    x in {1} by XBOOLE_0:def 4;
    then x in {1,2,3,4}/\{1} iff
    x=1 by TARSKI:def 1,ENUMSET1:def 2;
    hence x in {1,2,3,4}/\{1} iff
    x in {1} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL5:{1,2,3,4}/\{2} = {2}
proof
  now
    let x be object;
    x in {1,2,3,4}/\{2} iff x in {1,2,3,4} &
    x in {2} by XBOOLE_0:def 4;
    then x in {1,2,3,4}/\{2} iff
    x=2 by TARSKI:def 1,ENUMSET1:def 2;
    hence x in {1,2,3,4}/\{2} iff
    x in {2} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL6:{1,2,3,4}/\{3} = {3}
proof
  now
    let x be object;
    x in {1,2,3,4}/\{3} iff x in {1,2,3,4} &
    x in {3} by XBOOLE_0:def 4;
    then x in {1,2,3,4}/\{3} iff
    x=3 by TARSKI:def 1,ENUMSET1:def 2;
    hence x in {1,2,3,4}/\{3} iff
    x in {3} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL7:{1,2,3,4}/\{4} = {4}
proof
  now
    let x be object;
    x in {1,2,3,4}/\{4} iff x in {1,2,3,4} &
    x in {4} by XBOOLE_0:def 4;
    then x in {1,2,3,4}/\{4} iff
    x=4 by TARSKI:def 1,ENUMSET1:def 2;
    hence x in {1,2,3,4}/\{4} iff
    x in {4} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL10:{1,2,3}/\{2,3,4}={2,3}
proof
  now
    let x be object;
    x in {1,2,3}/\{2,3,4} iff x in {1,2,3} & x in {2,3,4} by XBOOLE_0:def 4;
    then x in {1,2,3}/\{2,3,4} iff (x=1 or x=2 or x=3) &
    (x=2 or x=3 or x=4) by ENUMSET1:def 1;
    hence x in {1,2,3}/\{2,3,4} iff x in {2,3} by TARSKI:def 2;
  end;
  hence thesis by TARSKI:2;
end;

LL11:{1,2,3}/\{1} = {1}
proof
  now
    let x be object;
    x in {1,2,3}/\{1} iff x in {1,2,3} &
    x in {1} by XBOOLE_0:def 4;
    then x in {1,2,3}/\{1} iff
    x=1 by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {1,2,3}/\{1} iff
    x in {1} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL12:{1,2,3}/\{2} = {2}
proof
  now
    let x be object;
    x in {1,2,3}/\{2} iff x in {1,2,3} &
    x in {2} by XBOOLE_0:def 4;
    then x in {1,2,3}/\{2} iff
    x=2 by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {1,2,3}/\{2} iff
    x in {2} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL13:{1,2,3}/\{3} = {3}
proof
  now
    let x be object;
    x in {1,2,3}/\{3} iff x in {1,2,3} &
    x in {3} by XBOOLE_0:def 4;
    then x in {1,2,3}/\{3} iff
    x=3 by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {1,2,3}/\{3} iff x in {3} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL14:{1,2,3}/\{4} = {}
proof
  now
    let x be object;
    x in {1,2,3}/\{4} iff x in {1,2,3} &
    x in {4} by XBOOLE_0:def 4;
    then x in {1,2,3}/\{4} iff (x=1 or x=2 or x=3) & x=4
    by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {1,2,3}/\{4} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

LL11a:{2,3,4}/\{1} = {}
proof
  now
    let x be object;
    x in {2,3,4}/\{1} iff x in {2,3,4} &
    x in {1} by XBOOLE_0:def 4;
    then x in {2,3,4}/\{1} iff (x=2 or x=3 or x=4) & x=1
    by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {2,3,4}/\{1} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

LL12a:{2,3,4}/\{2} = {2}
proof
  now
    let x be object;
    x in {2,3,4}/\{2} iff x in {2,3,4} &
    x in {2} by XBOOLE_0:def 4;
    then x in {2,3,4}/\{2} iff
    x=2 by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {2,3,4}/\{2} iff
    x in {2} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL13a:{2,3,4}/\{3} = {3}
proof
  now
    let x be object;
    x in {2,3,4}/\{3} iff x in {2,3,4} &
    x in {3} by XBOOLE_0:def 4;
    then x in {2,3,4}/\{3} iff
    x=3 by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {2,3,4}/\{3} iff x in {3} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL14a:{2,3,4}/\{4} = {4}
proof
  now
    let x be object;
    x in {2,3,4}/\{4} iff x in {2,3,4} &
    x in {4} by XBOOLE_0:def 4;
    then x in {2,3,4}/\{4} iff
    x=4 by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {2,3,4}/\{4} iff
    x in {4} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

LL17:{1}/\{2}={}
proof
  now
    let x be object;
    x in {1}/\{2} iff x in {1} & x in {2} by XBOOLE_0:def 4;
    then x in {1}/\{2} iff x=1 & x=2 by TARSKI:def 1;
    hence x in {1}/\{2} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

LL18:{1}/\{3}={}
proof
  now
    let x be object;
    x in {1}/\{3} iff x in {1} & x in {3} by XBOOLE_0:def 4;
    then x in {1}/\{3} iff x=1 & x=3 by TARSKI:def 1;
    hence x in {1}/\{3} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

LL19:{1}/\{4}={}
proof
  now
    let x be object;
    x in {1}/\{4} iff x in {1} & x in {4} by XBOOLE_0:def 4;
    then x in {1}/\{4} iff x=1 & x=4 by TARSKI:def 1;
    hence x in {1}/\{4} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

LL21:{2}/\{3}={}
proof
  now
    let x be object;
    x in {2}/\{3} iff x in {2} & x in {3} by XBOOLE_0:def 4;
    then x in {2}/\{3} iff x=2 & x=3 by TARSKI:def 1;
    hence x in {2}/\{3} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

LL22:{2}/\{4}={}
proof
  now
    let x be object;
    x in {2}/\{4} iff x in {2} & x in {4} by XBOOLE_0:def 4;
    then x in {2}/\{4} iff x=2 & x=4 by TARSKI:def 1;
    hence x in {2}/\{4} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

LL24:{3}/\{4}={}
proof
  now
    let x be object;
    x in {3}/\{4} iff x in {3} & x in {4} by XBOOLE_0:def 4;
    then x in {3}/\{4} iff x=3 & x=4 by TARSKI:def 1;
    hence x in {3}/\{4} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

Thm1:
  INTERSECTION(S,S)=
     {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}}
  proof
T1: INTERSECTION(S,S) c= {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},
    {},{2,3}}
    proof
      let s be object;
      assume s in INTERSECTION(S,S);
      then consider x,y be set such that
H2:   x in S and
H3:   y in S and
H4:   s=x/\y by SETFAM_1:def 5;
      (x= {1,2,3,4} or x={1,2,3} or x={2,3,4} or x={1} or x={2} or
      x={3} or x={4} or x={})& (y={1,2,3,4} or y={1,2,3} or y={2,3,4} or
      y={1} or y={2} or y={3} or y={4} or y={}) by H2,H3,ENUMSET1:def 6;
      hence thesis by LL2,LL3,LL4,LL5,LL6,LL7,LL10,
      LL11,LL12,LL13,LL14,LL17,LL18,LL19,LL21,LL22,LL24,
      LL11a,LL12a,LL13a,LL14a,H4,ENUMSET1:def 7;
    end;
    {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} c= INTERSECTION(S,S)
    proof
      let x be object;
      assume
B0:   x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}};
      {1,2,3,4} in S & {1,2,3} in S & {2,3,4} in S & {1} in S &
      {2} in S & {3} in S & {4} in S & {} in S by ENUMSET1:def 6;
      then {1,2,3,4}/\{1,2,3,4} in INTERSECTION(S,S) &
      {1,2,3}/\{1,2,3} in INTERSECTION(S,S) &
      {2,3,4}/\{2,3,4} in INTERSECTION(S,S) &
      {1}/\{1} in INTERSECTION(S,S) & {2}/\{2} in INTERSECTION(S,S) &
      {3}/\{3} in INTERSECTION(S,S) & {4}/\{4} in INTERSECTION(S,S) &
      {}/\{} in INTERSECTION(S,S) & {1,2,3}/\{2,3,4} in INTERSECTION(S,S)
      by SETFAM_1:def 5;
      hence thesis by LL10,B0,ENUMSET1:def 7;
    end;
    hence thesis by T1;
  end;

LemAA:
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}}=
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}}\/{{2,3}}
proof
  thus {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} c=
  {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}}\/{{2,3}}
  proof
    let x be object;
    assume x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}};
    then x={1,2,3,4} or x={1,2,3} or x={2,3,4} or x={1} or x= {2} or
    x={3} or x={4} or x={} or x={2,3} by ENUMSET1:def 7;
    then x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} or x in {{2,3}}
    by ENUMSET1:def 6,TARSKI:def 1;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}}\/{{2,3}};
  then x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} or x in {{2,3}}
  by XBOOLE_0:def 3;
  then x={1,2,3,4} or x={1,2,3} or x={2,3,4} or
  x={1} or x={2} or x={3} or x={4} or x={} or x ={2,3}
  by ENUMSET1:def 6,TARSKI:def 1;
  hence thesis by ENUMSET1:def 7;
end;

LemmeA:
  for x be non empty set st x in sring4_8 holds
  {x} is Subset of sring4_8 &
  {x} is a_partition of x
  proof
    let x be non empty set;
    assume x in S;
    then {x} c= S by TARSKI:def 1;
    hence thesis by EQREL_1:39;
  end;

Thm98:
  for x be set st x in sring4_8 ex P be finite Subset of sring4_8 st
  P is a_partition of x
  proof
    let x be set;
    assume
A0: x in S;
    per cases;
    suppose
C0:   x is empty;
      {} is Subset of S &
      {} is a_partition of {} by SUBSET_1:1,EQREL_1:45;
      hence thesis by C0;
    end;
    suppose x is non empty;
      then {x} is Subset of S & {x} is a_partition of x by A0,LemmeA;
      hence thesis;
    end;
  end;

Thm99:
  {{2},{3}} is Subset of sring4_8 & {{2},{3}} is a_partition of {2,3}
  proof
H1a: {{2},{3}} c= S
      proof
        let x be object;
        assume x in {{2},{3}};
        then x ={2} or x={3} by TARSKI:def 2;
        hence thesis by ENUMSET1:def 6;
      end;
H2: {{2},{3}} is Subset-Family of {2,3}
    proof
      {{2},{3}} c= bool {2,3}
      proof
        let x be object;
        assume x in {{2},{3}}; then
AAA:    x={2} or x={3} by TARSKI:def 2;
        {2} c= {2,3} & {3} c= {2,3} by ZFMISC_1:7;
        hence thesis by AAA;
      end;
      hence thesis;
    end;
H3: union {{2},{3}}={2,3} by ZFMISC_1:26;
    for x be Subset of {2,3} st x in {{2},{3}} holds x<>{} &
    for y be Subset of {2,3} st y in {{2},{3}} holds x=y or x misses y
    proof
      let x be Subset of {2,3};
      assume
AA0:  x in {{2},{3}};
      hence x<>{};
      for y be Subset of {2,3} st y in {{2},{3}} holds x=y or x misses y
      proof
        let y be Subset of {2,3};
        assume y in {{2},{3}};
        then (y={2} or y={3}) & (x={2} or x={3}) by AA0,TARSKI:def 2;
        hence thesis by LL21;
      end;
      hence thesis;
    end;
    hence thesis by H1a,H2,H3,EQREL_1:def 4;
  end;

LemC:
  for x be set st x in INTERSECTION(S,S) ex P be finite Subset of S st
  P is a_partition of x
  proof
    let x be set;
    assume x in INTERSECTION(S,S);
    then
H2: x in S or x in {{2,3}} by LemAA,Thm1,XBOOLE_0:def 3;
    x={2,3} implies ex P be finite Subset of S st P is a_partition of x
    by Thm99;
    hence thesis by H2,TARSKI:def 1,Thm98;
  end;

LemA:
  not {1,2,3}/\{2,3,4} in S
  proof
A1: {2,3} <> {1,2,3,4}
    proof
      assume {2,3}={1,2,3,4};
      then 1 in {2,3} by ENUMSET1:def 2;
      hence thesis by TARSKI:def 2;
    end;
A2: {2,3} <> {1,2,3}
    proof
      assume {2,3}={1,2,3};
      then 1 in {2,3} by ENUMSET1:def 1;
      hence thesis by TARSKI:def 2;
    end;
A3: {2,3} <> {2,3,4}
    proof
      assume {2,3}={2,3,4};
      then 4 in {2,3} by ENUMSET1:def 1;
      hence thesis by TARSKI:def 2;
    end;
A4: {2,3} <> {1} by ZFMISC_1:5;
A5: {2,3} <> {2} by ZFMISC_1:5;
A6: {2,3} <> {3} by ZFMISC_1:5;
    {2,3} <> {4} by ZFMISC_1:5;
    hence thesis by LL10,A1,A2,A3,A4,A5,A6,ENUMSET1:def 6;
  end;

registration
  cluster sring4_8 -> cap-finite-partition-closed non cap-closed;
  coherence
  proof
    sring4_8 is cap-finite-partition-closed
    proof
      let S1,S2 be Element of sring4_8;
      assume
      S1/\S2 is non empty;
      S1/\S2 in INTERSECTION(sring4_8,sring4_8) by SETFAM_1:def 5;
      then consider P be finite Subset of sring4_8 such that
A5:   P is a_partition of S1/\S2 by LemC;
      take P;
      thus thesis by A5;
    end;
    hence sring4_8 is cap-finite-partition-closed;
    assume
H2: S is cap-closed;
    {1,2,3} in S & {2,3,4} in S by ENUMSET1:def 6;
    hence thesis by LemA,H2,FINSUB_1:def 2;
  end;
end;

GG2: {1,2,3,4}\{1,2,3}={4}
  proof
    thus {1,2,3,4}\{1,2,3} c= {4}
    proof
      let x be object;
      assume x in {1,2,3,4}\{1,2,3};
      then x in {1,2,3,4} & not x in {1,2,3} by XBOOLE_0:def 5;
      then (x=1 or x=2 or x=3 or x=4) &
      not (x=1 or x=2 or x=3) by ENUMSET1:def 1,ENUMSET1:def 2;
      hence thesis by TARSKI:def 1;
    end;
    let x be object;
    assume x in {4};
    then x=4 by TARSKI:def 1;
    then x in {1,2,3,4} & not x in {1,2,3} by ENUMSET1:def 1,ENUMSET1:def 2;
    hence thesis by XBOOLE_0:def 5;
  end;

GG3:{1,2,3,4}\{2,3,4}={1}
  proof
    thus {1,2,3,4}\{2,3,4} c= {1}
    proof
      let x be object;
      assume x in {1,2,3,4}\{2,3,4};
      then x in {1,2,3,4} & not x in {2,3,4} by XBOOLE_0:def 5;
      then (x=1 or x=2 or x=3 or x=4) &
      not (x=2 or x=3 or x=4) by ENUMSET1:def 1,ENUMSET1:def 2;
      hence thesis by TARSKI:def 1;
    end;
    let x be object;
    assume x in {1};
    then x=1 by TARSKI:def 1;
    then x in {1,2,3,4} & not x in {2,3,4} by ENUMSET1:def 1,ENUMSET1:def 2;
    hence thesis by XBOOLE_0:def 5;
  end;

GG4:{1,2,3,4}\{1}={2,3,4}
proof
  thus {1,2,3,4}\{1} c= {2,3,4}
  proof
    let x be object;
    assume x in {1,2,3,4}\{1};
    then x in {1,2,3,4} & not x in {1} by XBOOLE_0:def 5;
    then (x=1 or x=2 or x=3 or x=4) &
    not (x=1) by ENUMSET1:def 2,TARSKI:def 1;
    hence thesis by ENUMSET1:def 1;
  end;
  let x be object;
  assume x in {2,3,4};
  then x=2 or x=3 or x=4 by ENUMSET1:def 1;
  then x in {1,2,3,4} & not x in {1} by TARSKI:def 1,ENUMSET1:def 2;
  hence thesis by XBOOLE_0:def 5;
end;

GG5:{1,2,3,4}\{2}={1,3,4}
proof
  thus {1,2,3,4}\{2} c= {1,3,4}
  proof
    let x be object;
    assume x in {1,2,3,4}\{2};
    then x in {1,2,3,4} & not x in {2} by XBOOLE_0:def 5;
    then (x=1 or x=2 or x=3 or x=4) &
    not (x=2) by ENUMSET1:def 2,TARSKI:def 1;
    hence thesis by ENUMSET1:def 1;
  end;
  let x be object;
  assume x in {1,3,4};
  then x=1 or x=3 or x=4 by ENUMSET1:def 1;
  then x in {1,2,3,4} & not x in {2} by TARSKI:def 1,ENUMSET1:def 2;
  hence thesis by XBOOLE_0:def 5;
end;

GG6:{1,2,3,4}\{3}={1,2,4}
proof
  thus {1,2,3,4}\{3} c= {1,2,4}
  proof
    let x be object;
    assume x in {1,2,3,4}\{3};
    then x in {1,2,3,4} & not x in {3} by XBOOLE_0:def 5;
    then (x=1 or x=2 or x=3 or x=4) &
    not x=3 by ENUMSET1:def 2,TARSKI:def 1;
    hence thesis by ENUMSET1:def 1;
  end;
  let x be object;
  assume x in {1,2,4};
  then x=1 or x=2 or x=4 by ENUMSET1:def 1;
  then x in {1,2,3,4} & not x in {3} by TARSKI:def 1,ENUMSET1:def 2;
  hence thesis by XBOOLE_0:def 5;
end;

GG7:{1,2,3,4}\{4}={1,2,3}
proof
  thus {1,2,3,4}\{4} c= {1,2,3}
  proof
    let x be object;
    assume x in {1,2,3,4}\{4};
    then x in {1,2,3,4} & not x in {4} by XBOOLE_0:def 5;
    then (x=1 or x=2 or x=3 or x=4) &
    not x=4 by ENUMSET1:def 2,TARSKI:def 1;
    hence thesis by ENUMSET1:def 1;
  end;
  let x be object;
  assume x in {1,2,3};
  then x=1 or x=2 or x=3 by ENUMSET1:def 1;
  then x in {1,2,3,4} & not x in {4} by TARSKI:def 1,ENUMSET1:def 2;
  hence thesis by XBOOLE_0:def 5;
end;

GG11:{1,2,3}\{2,3,4}={1}
proof
  thus {1,2,3}\{2,3,4} c= {1}
  proof
    let x be object;
    assume x in {1,2,3}\{2,3,4};
    then x in {1,2,3} & not x in {2,3,4} by XBOOLE_0:def 5;
    then (x=1 or x=2 or x=3) &
    not (x=2 or x=3 or x=4) by ENUMSET1:def 1;
    hence thesis by TARSKI:def 1;
  end;
  let x be object;
  assume x in {1};
  then x=1 by TARSKI:def 1;
  then x in {1,2,3} & not x in {2,3,4} by ENUMSET1:def 1;
  hence thesis by XBOOLE_0:def 5;
end;

GG12:{1,2,3}\{1}={2,3}
proof
  now
    let x be object;
    x in {1,2,3}\{1} iff x in {1,2,3} & not x in {1} by XBOOLE_0:def 5;
    then x in {1,2,3}\{1} iff (x=1 or x=2 or x=3) & not x=1
    by ENUMSET1:def 1,TARSKI:def 1;
    hence x in {1,2,3}\{1} iff x in {2,3} by TARSKI:def 2;
  end;
  hence thesis by TARSKI:2;
end;

GG13:{1,2,3}\{2}={1,3}
proof
  now
    let x be object;
    x in {1,2,3}\{2} iff x in {1,2,3} & not x in {2} by XBOOLE_0:def 5;
    then x in {1,2,3}\{2} iff (x=1 or x=2 or x=3) & not x=2
    by ENUMSET1:def 1,TARSKI:def 1;
    hence x in {1,2,3}\{2} iff x in {1,3} by TARSKI:def 2;
  end;
  hence thesis by TARSKI:2;
end;

GG14:{1,2,3}\{3}={1,2}
proof
  now
    let x be object;
    x in {1,2,3}\{3} iff x in {1,2,3} & not x in {3} by XBOOLE_0:def 5;
    then x in {1,2,3}\{3} iff (x=1 or x=2 or x=3) & not x=3
    by ENUMSET1:def 1,TARSKI:def 1;
    hence x in {1,2,3}\{3} iff x in {1,2} by TARSKI:def 2;
  end;
  hence thesis by TARSKI:2;
end;

GG15:{1,2,3}\{4}={1,2,3}
proof
  now
    let x be object;
    x in {1,2,3}\{4} iff x in {1,2,3} & not x in {4} by XBOOLE_0:def 5;
    then x in {1,2,3}\{4} iff (x=1 or x=2 or x=3) & not x=4
    by ENUMSET1:def 1,TARSKI:def 1;
    hence x in {1,2,3}\{4} iff x in {1,2,3} by ENUMSET1:def 1;
  end;
  hence thesis by TARSKI:2;
end;

GG18:{2,3,4}\{1,2,3}={4}
proof
  now
    let x be object;
    x in {2,3,4}\{1,2,3} iff x in {2,3,4} & not x in {1,2,3} by XBOOLE_0:def 5;
    then x in {2,3,4}\{1,2,3} iff (x=2 or x=3 or x=4) & not (x=1 or x=2 or x=3)
    by ENUMSET1:def 1;
    hence x in {2,3,4}\{1,2,3} iff x in {4} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

GG20:{2,3,4}\{1}={2,3,4}
proof
  now
    let x be object;
    x in {2,3,4}\{1} iff x in {2,3,4} & not x in {1} by XBOOLE_0:def 5;
    then x in {2,3,4}\{1} iff (x=2 or x=3 or x=4) & not x=1
    by ENUMSET1:def 1,TARSKI:def 1;
    hence x in {2,3,4}\{1} iff x in {2,3,4} by ENUMSET1:def 1;
  end;
  hence thesis by TARSKI:2;
end;

GG21:{2,3,4}\{2}={3,4}
proof
  now
    let x be object;
    x in {2,3,4}\{2} iff x in {2,3,4} & not x in {2} by XBOOLE_0:def 5;
    then x in {2,3,4}\{2} iff (x=2 or x=3 or x=4) & not x=2
    by ENUMSET1:def 1,TARSKI:def 1;
    hence x in {2,3,4}\{2} iff x in {3,4} by TARSKI:def 2;
  end;
  hence thesis by TARSKI:2;
end;

GG22:{2,3,4}\{3}={2,4}
proof
  now
    let x be object;
    x in {2,3,4}\{3} iff x in {2,3,4} & not x in {3} by XBOOLE_0:def 5;
    then x in {2,3,4}\{3} iff (x=2 or x=3 or x=4) & not x=3
    by ENUMSET1:def 1,TARSKI:def 1;
    hence x in {2,3,4}\{3} iff x in {2,4} by TARSKI:def 2;
  end;
  hence thesis by TARSKI:2;
end;

GG23:{2,3,4}\{4}={2,3}
proof
  now
    let x be object;
    x in {2,3,4}\{4} iff x in {2,3,4} & not x in {4} by XBOOLE_0:def 5;
    then x in {2,3,4}\{4} iff (x=2 or x=3 or x=4) & not x=4
    by ENUMSET1:def 1,TARSKI:def 1;
    hence x in {2,3,4}\{4} iff x in {2,3} by TARSKI:def 2;
  end;
  hence thesis by TARSKI:2;
end;

GG27:{1}\{2,3,4}={1}
proof
  now
    let x be object;
    x in {1}\{2,3,4} iff x in {1} & not x in {2,3,4} by XBOOLE_0:def 5;
    then x in {1}\{2,3,4} iff x=1 & not (x=2 or x=3 or x=4)
    by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {1}\{2,3,4} iff x in {1} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

GG33:{2}\{1,2,3,4}={}
proof
  now
    let x be object;
    x in {2}\{1,2,3,4} iff x in {2} & not x in {1,2,3,4} by XBOOLE_0:def 5;
    then x in {2}\{1,2,3,4} iff x=2 & not (x=1 or x=2 or x=3 or x=4)
    by TARSKI:def 1,ENUMSET1:def 2;
    hence x in {2}\{1,2,3,4} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

GG34:{2}\{1,2,3}={}
proof
  now
    let x be object;
    x in {2}\{1,2,3} iff x in {2} & not x in {1,2,3} by XBOOLE_0:def 5;
    then x in {2}\{1,2,3} iff x=2 & not (x=1 or x=2 or x=3)
    by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {2}\{1,2,3} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

GG35:{2}\{2,3,4}={}
proof
  now
    let x be object;
    x in {2}\{2,3,4} iff x in {2} & not x in {2,3,4} by XBOOLE_0:def 5;
    then x in {2}\{2,3,4} iff x=2 & not (x=2 or x=3 or x=4)
    by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {2}\{2,3,4} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

GG41:{3}\{1,2,3,4}={}
proof
  now
    let x be object;
    x in {3}\{1,2,3,4} iff x in {3} & not x in {1,2,3,4} by XBOOLE_0:def 5;
    then x in {3}\{1,2,3,4} iff x=3 & not (x=1 or x=2 or x=3 or x=4)
    by TARSKI:def 1,ENUMSET1:def 2;
    hence x in {3}\{1,2,3,4} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

GG42:{3}\{1,2,3}={}
proof
  now
    let x be object;
    x in {3}\{1,2,3} iff x in {3} & not x in {1,2,3} by XBOOLE_0:def 5;
    then x in {3}\{1,2,3} iff x=3 & not (x=1 or x=2 or x=3)
    by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {3}\{1,2,3} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

GG43:{3}\{2,3,4}={}
proof
  now
    let x be object;
    x in {3}\{2,3,4} iff x in {3} & not x in {2,3,4} by XBOOLE_0:def 5;
    then x in {3}\{2,3,4} iff x=3 & not (x=2 or x=3 or x=4)
    by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {3}\{2,3,4} iff contradiction;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

GG50:{4}\{1,2,3}={4}
proof
  now
    let x be object;
    x in {4}\{1,2,3} iff x in {4} & not x in {1,2,3} by XBOOLE_0:def 5;
    then x in {4}\{1,2,3} iff x=4 & not (x=1 or x=2 or x=3)
    by TARSKI:def 1,ENUMSET1:def 1;
    hence x in {4}\{1,2,3} iff x in {4} by TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

Thm50:
  DIFFERENCE(sring4_8,sring4_8) =
  sring4_8 \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}}
  proof
    thus DIFFERENCE(S,S) c=
    S \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}}
    proof
      let s be object;
      assume s in DIFFERENCE(S,S);
      then consider x,y be set such that
A1:   x in S & y in S and
A2:   s=x\y by SETFAM_1:def 6;
      (x= {1,2,3,4} or x={1,2,3} or x={2,3,4} or x={1} or x={2} or
      x={3} or x={4} or x={})& (y={1,2,3,4} or
      y={1,2,3} or y={2,3,4} or y={1} or y={2} or
      y={3} or y={4} or y={}) by A1,ENUMSET1:def 6; then
      s={1,2,3,4} or s={1,2,3} or s={2,3,4} or s={1} or s={2} or s={3} or
      s={4} or
      s={} or s={1,3,4} or s={1,2,4} or s={2,3} or s={1,3} or s={1,2} or
      s={3,4} or s={2,4} or s={2,3} or s={}
      by GG2,GG3,GG4,GG5,GG6,GG7,XBOOLE_1:37,
      GG11,GG12,GG13,GG14,GG15,GG18,GG20,
      GG21,GG22,GG23,GG27,ZFMISC_1:14,
      GG33,GG34,GG35,GG41,GG42,GG43,GG50,A2;
      then s in S or s in {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}}
      by ENUMSET1:def 6,def 5;
      hence thesis by XBOOLE_0:def 3;
    end;
      let s be object;
      assume s in S \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}};
      then s in S or
      s in {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} by XBOOLE_0:def 3;
      then
VU:   s={1,2,3,4}\{} or s={1,2,3}\{} or s={2,3,4}\{} or s={1}\{} or
      s={2}\{} or s={3}\{} or
      s={4}\{} or s={}\{} or
      s={1}\{1} or s={1,2,3,4}\{2} or s={1,2,3,4}\{3} or s={1,2,3}\{1} or
      s={1,2,3}\{2} or s={1,2,3}\{3} or s={2,3,4}\{2} or
      s={1,2,3}\{2,3,4} or s={2,3,4}\{3} or s={1,2,3}\{1}
      by GG5,GG6,GG12,GG13,GG14,
      GG21,GG22,ENUMSET1:def 6,ENUMSET1:def 5;
      {1,2,3,4} in S & {1,2,3} in S & {2,3,4} in S & {1} in S &
      {2} in S & {3} in S & {4} in S & {} in S by ENUMSET1:def 6;
      hence thesis by VU,SETFAM_1:def 6;
  end;

ThmV1:
  {{1},{3}} is Subset of sring4_8 & {{1},{3}} is a_partition of {1,3}
  proof
H1a: {{1},{3}} c= S
      proof
        let x be object;
        assume x in {{1},{3}};
        then x ={1} or x={3} by TARSKI:def 2;
        hence thesis by ENUMSET1:def 6;
    end;
H2: {{1},{3}} is Subset-Family of {1,3}
    proof
      {{1},{3}} c= bool {1,3}
      proof
        let x be object;
        assume x in {{1},{3}}; then
AAA:    x={1} or x={3} by TARSKI:def 2;
        {1} c= {1,3} & {3} c= {1,3} by ZFMISC_1:7;
        hence thesis by AAA;
      end;
      hence thesis;
    end;
H3: union {{1},{3}}={1,3} by ZFMISC_1:26;
    for x be Subset of {1,3} st x in {{1},{3}} holds x<>{} &
    for y be Subset of {1,3} st y in {{1},{3}} holds x=y or x misses y
    proof
      let x be Subset of {1,3};
      assume
AA0:  x in {{1},{3}};
      hence x<>{};
      for y be Subset of {1,3} st y in {{1},{3}} holds x=y or x misses y
      proof
        let y be Subset of {1,3};
        assume y in {{1},{3}};
        then (y={1} or y={3}) & (x={1} or x={3}) by AA0,TARSKI:def 2;
        hence thesis by LL18;
      end;
      hence thesis;
    end;
    hence thesis by H1a,H2,H3,EQREL_1:def 4;
  end;

ThmV2:
  {{1},{2}} is Subset of sring4_8 & {{1},{2}} is a_partition of {1,2}
  proof
H1a: {{1},{2}} c= S
      proof
        let x be object;
        assume x in {{1},{2}};
        then x ={1} or x={2} by TARSKI:def 2;
        hence thesis by ENUMSET1:def 6;
      end;
H2: {{1},{2}} is Subset-Family of {1,2}
    proof
      {{1},{2}} c= bool {1,2}
      proof
        let x be object;
        assume x in {{1},{2}};
        then
AAA:    x={1} or x={2} by TARSKI:def 2;
        {1} c= {1,2} & {2} c= {1,2} by ZFMISC_1:7;
        hence thesis by AAA;
      end;
      hence thesis;
    end;
H3: union {{1},{2}}={1,2} by ZFMISC_1:26;
    for x be Subset of {1,2} st x in {{1},{2}} holds x<>{} &
    for y be Subset of {1,2} st y in {{1},{2}} holds x=y or x misses y
    proof
      let x be Subset of {1,2};
      assume
AA0:  x in {{1},{2}};
      hence x<>{};
      for y be Subset of {1,2} st y in {{1},{2}} holds x=y or x misses y
      proof
        let y be Subset of {1,2};
        assume y in {{1},{2}};
        then (y={1} or y={2}) & (x={1} or x={2}) by AA0,TARSKI:def 2;
        hence thesis by LL17;
      end;
      hence thesis;
    end;
    hence thesis by H1a,H2,H3,EQREL_1:def 4;
  end;

ThmV3:
  {{2},{4}} is Subset of sring4_8 & {{2},{4}} is a_partition of {2,4}
  proof
H1a: {{2},{4}} c= S
      proof
        let x be object;
        assume x in {{2},{4}};
        then x ={2} or x={4} by TARSKI:def 2;
        hence thesis by ENUMSET1:def 6;
      end;
H2: {{2},{4}} is Subset-Family of {2,4}
    proof
      {{2},{4}} c= bool {2,4}
      proof
        let x be object;
        assume x in {{2},{4}}; then
AAA:    x={2} or x={4} by TARSKI:def 2;
        {2} c= {2,4} & {4} c= {2,4} by ZFMISC_1:7;
        hence thesis by AAA;
      end;
      hence thesis;
    end;
H3: union {{2},{4}}={2,4} by ZFMISC_1:26;
    for x be Subset of {2,4} st x in {{2},{4}} holds x<>{} &
    for y be Subset of {2,4} st y in {{2},{4}} holds x=y or x misses y
    proof
      let x be Subset of {2,4};
      assume
AA0:  x in {{2},{4}};
      hence x<>{};
      for y be Subset of {2,4} st y in {{2},{4}} holds x=y or x misses y
      proof
        let y be Subset of {2,4};
        assume y in {{2},{4}};
        then (y={2} or y={4}) & (x={2} or x={4}) by AA0,TARSKI:def 2;
        hence thesis by LL22;
      end;
      hence thesis;
    end;
    hence thesis by H1a,H2,H3,EQREL_1:def 4;
  end;

ThmV4:
  {{3},{4}} is Subset of sring4_8 & {{3},{4}} is a_partition of {3,4}
  proof
H1a: {{3},{4}} c= S
      proof
        let x be object;
        assume x in {{3},{4}};
        then x ={3} or x={4} by TARSKI:def 2;
        hence thesis by ENUMSET1:def 6;
      end;
H2: {{3},{4}} is Subset-Family of {3,4}
    proof
      {{3},{4}} c= bool {3,4}
      proof
        let x be object;
        assume x in {{3},{4}};
        then
AAA:    x={3} or x={4} by TARSKI:def 2;
        {3} c= {3,4} & {4} c= {3,4} by ZFMISC_1:7;
        hence thesis by AAA;
      end;
      hence thesis;
    end;
H3: union {{3},{4}}={3,4} by ZFMISC_1:26;
    for x be Subset of {3,4} st x in {{3},{4}} holds x<>{} &
    for y be Subset of {3,4} st y in {{3},{4}} holds x=y or x misses y
    proof
      let x be Subset of {3,4};
      assume
AA0:  x in {{3},{4}};
      hence x<>{};
      for y be Subset of {3,4} st y in {{3},{4}} holds x=y or x misses y
      proof
        let y be Subset of {3,4};
        assume y in {{3},{4}};
        then (y={3} or y={4}) & (x={3} or x={4}) by AA0,TARSKI:def 2;
        hence thesis by LL24;
      end;
      hence thesis;
    end;
    hence thesis by H1a,H2,H3,EQREL_1:def 4;
  end;

ThmV5:
  {{1},{3},{4}} is Subset of sring4_8 &
  {{1},{3},{4}} is a_partition of {1,3,4}
  proof
H1a: {{1},{3},{4}} c= S
      proof
        let x be object;
        assume x in {{1},{3},{4}};
        then x={1} or x={3} or x={4} by ENUMSET1:def 1;
        hence thesis by ENUMSET1:def 6;
      end;
H2: {{1},{3},{4}} is Subset-Family of {1,3,4}
    proof
      {{1},{3},{4}} c= bool {1,3,4}
      proof
        let x be object;
        assume x in {{1},{3},{4}};
        then
AAA:    x={1} or x={3} or x={4} by ENUMSET1:def 1;
        {1} c= {1,3,4} & {3} c= {1,3,4} & {4} c= {1,3,4}
        proof
          thus {1} c= {1,3,4}
          proof
            let x be object;
            assume x in {1};
            then x=1 by TARSKI:def 1;
            hence thesis by ENUMSET1:def 1;
          end;
          thus {3} c= {1,3,4}
          proof
            let x be object;
            assume x in {3};
            then x=3 by TARSKI:def 1;
            hence thesis by ENUMSET1:def 1;
          end;
          let x be object;
          assume x in {4};
          then x = 4 by TARSKI:def 1;
          hence thesis by ENUMSET1:def 1;
        end;
        hence thesis by AAA;
      end;
      hence thesis;
    end;
H3: union {{1},{3},{4}}={1,3,4}
    proof
T1:   union {{1}} = {1} & union {{3},{4}}={3,4}
      by ZFMISC_1:26;
T1A:  union {{1},{3},{4}}=union ({{1}}\/{{3},{4}}) by ENUMSET1:2;
      {1}\/{3,4}={1,3,4} by ENUMSET1:2;
      hence thesis by T1,T1A,ZFMISC_1:78;
    end;
    for x be Subset of {1,3,4} st x in {{1},{3},{4}} holds x<>{} &
    for y be Subset of {1,3,4} st y in {{1},{3},{4}} holds x=y or x misses y
    proof
      let x be Subset of {1,3,4};
      assume
AA0:  x in {{1},{3},{4}};
      hence x<>{};
      for y be Subset of {1,3,4} st y in {{1},{3},{4}} holds x=y or x misses y
      proof
        let y be Subset of {1,3,4};
        assume y in {{1},{3},{4}};
        then (y={1} or y={3} or y={4}) & (x={1} or x={3} or x={4})
        by AA0,ENUMSET1:def 1;
        hence thesis by LL18,LL19,LL24;
      end;
      hence thesis;
    end;
    hence thesis by H1a,H2,H3,EQREL_1:def 4;
  end;

ThmV6:
  {{1},{2},{4}} is Subset of sring4_8 &
  {{1},{2},{4}} is a_partition of {1,2,4}
  proof
H1a: {{1},{2},{4}} c= S
      proof
        let x be object;
        assume x in {{1},{2},{4}};
        then x={1} or x={2} or x={4} by ENUMSET1:def 1;
        hence thesis by ENUMSET1:def 6;
      end;
H2: {{1},{2},{4}} is Subset-Family of {1,2,4}
    proof
      {{1},{2},{4}} c= bool {1,2,4}
      proof
        let x be object;
        assume x in {{1},{2},{4}}; then
AAA:    x={1} or x={2} or x={4} by ENUMSET1:def 1;
        {1} c= {1,2,4} & {2} c= {1,2,4} & {4} c= {1,2,4}
        proof
          thus {1} c= {1,2,4}
          proof
            let x be object;
            assume x in {1};
            then x=1 by TARSKI:def 1;
            hence thesis by ENUMSET1:def 1;
          end;
          thus {2} c={1,2,4}
          proof
            let x be object;
            assume x in {2};
            then x=2 by TARSKI:def 1;
            hence thesis by ENUMSET1:def 1;
          end;
          let x be object;
          assume x in {4};
          then x = 4 by TARSKI:def 1;
          hence thesis by ENUMSET1:def 1;
        end;
        hence thesis by AAA;
      end;
      hence thesis;
    end;
H3: union {{1},{2},{4}}={1,2,4}
    proof
T1:   union {{1}} = {1} & union {{2},{4}}={2,4} by ZFMISC_1:26;
T1A:  {{1},{2},{4}}={{1}}\/{{2},{4}} by ENUMSET1:2;
      {1}\/{2,4}={1,2,4} by ENUMSET1:2;
      hence thesis by T1,T1A,ZFMISC_1:78;
    end;
    for x be Subset of {1,2,4} st x in {{1},{2},{4}} holds x<>{} &
    for y be Subset of {1,2,4} st y in {{1},{2},{4}} holds x=y or x misses y
    proof
      let x be Subset of {1,2,4};
      assume
AA0:  x in {{1},{2},{4}};
      hence x<>{};
      for y be Subset of {1,2,4} st y in {{1},{2},{4}} holds x=y or x misses y
      proof
        let y be Subset of {1,2,4};
        assume y in {{1},{2},{4}};
        then (y={1} or y={2} or y={4}) & (x={1} or x={2} or x={4})
        by AA0,ENUMSET1:def 1;
        hence thesis by LL17,LL19,LL22;
      end;
      hence thesis;
    end;
    hence thesis by H1a,H2,H3,EQREL_1:def 4;
  end;

LemD:
  for x be set st x in DIFFERENCE(S,S) ex P be finite Subset of S st
  P is a_partition of x
  proof
    let x be set;
    assume x in DIFFERENCE(S,S); then
    x in S or x in {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}}
    by Thm50,XBOOLE_0:def 3;
    then per cases by ENUMSET1:def 5;
    suppose x in S;
      hence thesis by Thm98;
    end;
    suppose x={2,3};
      hence thesis by Thm99;
    end;
    suppose x={1,3};
      hence thesis by ThmV1;
    end;
    suppose x={1,2};
      hence thesis by ThmV2;
    end;
    suppose x={3,4};
      hence thesis by ThmV4;
    end;
    suppose x={2,4};
      hence thesis by ThmV3;
    end;
    suppose x={1,3,4};
      hence thesis by ThmV5;
    end;
    suppose x={1,2,4};
      hence thesis by ThmV6;
    end;
  end;

registration
  cluster sring4_8 -> diff-finite-partition-closed;
  coherence
  proof
    for y,z be Element of sring4_8 st y\z is non empty holds
    ex P be finite Subset of sring4_8 st P is a_partition of y\z
    proof
       let y,z be Element of sring4_8;
       assume y\z is non empty;
       y\z in DIFFERENCE(sring4_8,sring4_8) by SETFAM_1:def 6;
       hence thesis by LemD;
    end;
    hence thesis by SRINGS_1:def 2;
  end;
end;