:: Basic Properties of Rough Sets and Rough Membership Function
::  by Adam Grabowski
::
:: Received November 23, 2003
:: Copyright (c) 2003-2012 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 NUMBERS, ORDERS_2, RELAT_1, NATTRA_1, TOLER_1, TARSKI, ZFMISC_1,
      MATRIX_1, STRUCT_0, RELAT_2, XBOOLE_0, PARTFUN1, SUBSET_1, FINSEQ_1,
      CARD_3, ORDINAL4, FUNCT_1, PROB_2, FINSEQ_2, NAT_1, FINSET_1, EQREL_1,
      CARD_1, ARYTM_3, XXREAL_0, XXREAL_1, FUNCT_3, ARYTM_1, ROUGHS_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, NUMBERS, XCMPLX_0,
      ORDINAL1, XXREAL_0, FINSET_1, RELAT_1, RELAT_2, FUNCT_1, FINSEQ_1,
      RVSUM_1, FINSEQ_2, RELSET_1, PARTFUN1, CARD_3, PROB_2, FUNCT_2, FUNCT_3,
      DOMAIN_1, STRUCT_0, ORDERS_2, EQREL_1, RCOMP_1, TOLER_1, ORDERS_3;
 constructors EQREL_1, PROB_2, RCOMP_1, RVSUM_1, FUNCT_6, REALSET2, ORDERS_3,
      RELSET_1, BINOP_2;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FINSET_1, NUMBERS,
      XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, EQREL_1, STRUCT_0,
      ORDERS_2, VALUED_0, CARD_1, RELSET_1;
 requirements BOOLE, SUBSET, NUMERALS, REAL;
 definitions TARSKI, XBOOLE_0, PROB_2, FINSEQ_2, SUBSET_1, CARD_3, STRUCT_0;
 theorems EQREL_1, XBOOLE_0, XBOOLE_1, SUBSET_1, XCMPLX_1, CARD_2, CARD_1,
      TOLER_1, NAT_1, TARSKI, ZFMISC_1, RELAT_1, RELAT_2, ORDERS_3, CHAIN_1,
      FUNCT_2, FUNCT_3, RVSUM_1, FINSEQ_1, FINSEQ_3, PROB_2, FUNCT_1, GRFUNC_1,
      FINSEQ_6, FINSEQ_2, ORDERS_2, SYSREL, FUNCOP_1, ORDERS_1, XREAL_0,
      ORDINAL1, XXREAL_1, XREAL_1, XXREAL_0, PRE_POLY;
 schemes FUNCT_2, BINOP_2, FINSEQ_2;

begin :: Preliminaries

registration
  let A be set;
  cluster RelStr (# A, id A #) -> discrete;
  coherence by ORDERS_3:def 1;
end;

theorem Th1:
  for X being set st Total X c= id X holds X is trivial
proof
  let X be set;
  assume
A1: Total X c= id X;
  assume X is non trivial;
  then consider x, y being set such that
A2: x in X & y in X and
A3: x <> y by ZFMISC_1:def 10;
  [x,y] in Total X by A2,TOLER_1:2;
  hence thesis by A1,A3,RELAT_1:def 10;
end;

definition
  let A be RelStr;
  attr A is diagonal means
  :Def1:
  the InternalRel of A c= id the carrier of A;
end;

registration
  let A be non trivial set;
  cluster RelStr (# A, Total A #) -> non diagonal;
  coherence
  proof
    not Total A c= id A by Th1;
    hence thesis by Def1;
  end;
end;

theorem
  for L being reflexive RelStr holds id the carrier of L c= the
  InternalRel of L
proof
  let L be reflexive RelStr;
  for a,b being set st [a,b] in id the carrier of L holds [a,b] in the
  InternalRel of L
  proof
    let a,b be set;
    assume [a,b] in id the carrier of L;
    then
A1: a = b & a in the carrier of L by RELAT_1:def 10;
    the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;
    hence thesis by A1,RELAT_2:def 1;
  end;
  hence thesis by RELAT_1:def 3;
end;

Lm1: for A being RelStr st A is reflexive trivial holds A is discrete
proof
  let A be RelStr;
  assume
A1: A is reflexive trivial;
  per cases by A1,ZFMISC_1:131;
  suppose
A2: the carrier of A is empty;
    then the InternalRel of A = {};
    hence thesis by A2,ORDERS_3:def 1,RELAT_1:55;
  end;
  suppose
    ex x being set st the carrier of A = {x};
    then consider x being set such that
A3: the carrier of A = {x};
    the InternalRel of A c= [:{x}, {x}:] by A3;
    then the InternalRel of A c= { [x, x] } by ZFMISC_1:29;
    then
A4: the InternalRel of A = { [x, x] } or the InternalRel of A = {} by
ZFMISC_1:33;
A5: the InternalRel of A is_reflexive_in the carrier of A by A1,ORDERS_2:def 2;
    x in the carrier of A by A3,TARSKI:def 1;
    then the InternalRel of A = id {x} by A4,A5,RELAT_2:def 1,SYSREL:13;
    hence thesis by A3,ORDERS_3:def 1;
  end;
end;

registration
  cluster non discrete -> non trivial for reflexive RelStr;
  coherence by Lm1;
  cluster reflexive trivial -> discrete for RelStr;
  coherence;
end;

theorem
  for X being set, R being total reflexive Relation of X holds id X c= R
proof
  let X be set, R be total reflexive Relation of X;
  field R = X by ORDERS_1:12;
  hence thesis by RELAT_2:1;
end;

Lm2: for A being RelStr st A is discrete holds A is diagonal
proof
  let A be RelStr;
  assume A is discrete;
  then the InternalRel of A = id the carrier of A by ORDERS_3:def 1;
  hence thesis by Def1;
end;

registration
  cluster discrete -> diagonal for RelStr;
  coherence by Lm2;
  cluster non diagonal -> non discrete for RelStr;
  coherence;
end;

registration
  cluster non diagonal non empty for RelStr;
  existence
  proof
    set A = the non trivial set;
    take RelStr (# A, Total A #);
    thus thesis;
  end;
end;

theorem Th4:
  for A being non diagonal non empty RelStr ex x, y being Element
  of A st x <> y & [x,y] in the InternalRel of A
proof
  let A be non diagonal non empty RelStr;
  now
    assume
A1: for x,y being Element of A st [x,y] in the InternalRel of A holds x = y;
    for a,b being set st [a,b] in the InternalRel of A holds [a,b] in id
    the carrier of A
    proof
      let a,b be set;
      assume
A2:   [a,b] in the InternalRel of A;
      then
A3:   a is Element of A by ZFMISC_1:87;
      b is Element of A by A2,ZFMISC_1:87;
      then a = b by A1,A2,A3;
      hence thesis by A3,RELAT_1:def 10;
    end;
    then the InternalRel of A c= id the carrier of A by RELAT_1:def 3;
    hence thesis by Def1;
  end;
  hence thesis;
end;

theorem Th5:
  for D being set, p, q being FinSequence of D holds Union (p^q) =
  Union p \/ Union q
proof
  let D be set, p, q be FinSequence of D;
  union rng(p^q) = union (rng p \/ rng q) by FINSEQ_1:31
    .= Union p \/ Union q by ZFMISC_1:78;
  hence thesis;
end;

theorem Th6:
  for p, q being Function st q is disjoint_valued & p c= q holds p
  is disjoint_valued
proof
  let p, q be Function;
  assume that
A1: q is disjoint_valued and
A2: p c= q;
  for x, y being set st x <> y holds p.x misses p.y
  proof
    let x, y be set;
    assume
A3: x <> y;
    assume
A4: p.x meets p.y;
    x in dom p & y in dom p
    proof
      assume not x in dom p or not y in dom p;
      then p.x = {} or p.y = {} by FUNCT_1:def 2;
      hence thesis by A4,XBOOLE_1:65;
    end;
    then p.x = q.x & p.y = q.y by A2,GRFUNC_1:2;
    hence thesis by A1,A3,A4,PROB_2:def 2;
  end;
  hence thesis by PROB_2:def 2;
end;

registration
  cluster empty -> disjoint_valued for Function;
  coherence
  proof
    let X be Function;
    assume
A1: X is empty;
    X is disjoint_valued
    proof
      let x, y be set;
      assume x <> y;
      X.x = {} by A1,FUNCT_1:def 2,RELAT_1:38;
      hence thesis by XBOOLE_1:65;
    end;
    hence thesis;
  end;
end;

registration
  let A be set;
  cluster disjoint_valued for FinSequence of A;
  existence
  proof
    set X = <*>A;
    X is disjoint_valued;
    hence thesis;
  end;
end;

registration
  let A be non empty set;
  cluster non empty disjoint_valued for FinSequence of A;
  existence
  proof
    set a = the Element of A;
    reconsider X = 1 |-> a as FinSequence of A;
A1: X is disjoint_valued
    proof
      let x, y be set;
      assume
A2:   x <> y;
      per cases;
      suppose
A3:     x in dom X & y in dom X;
        then x in Seg 1 by FUNCOP_1:13;
        then
A4:     x = 1 by FINSEQ_1:2,TARSKI:def 1;
        y in Seg 1 by A3,FUNCOP_1:13;
        hence thesis by A2,A4,FINSEQ_1:2,TARSKI:def 1;
      end;
      suppose
        not x in dom X or not y in dom X;
        then X.x = {} or X.y = {} by FUNCT_1:def 2;
        hence thesis by XBOOLE_1:65;
      end;
    end;
    X is non empty by FUNCOP_1:13,RELAT_1:38;
    hence thesis by A1;
  end;
end;

definition
  let A be set;
  let X be FinSequence of bool A;
  let n be Nat;
  redefine func X.n -> Subset of A;
  coherence
  proof
    per cases;
    suppose
      not n in dom X;
      then X.n = {} by FUNCT_1:def 2;
      hence thesis by XBOOLE_1:2;
    end;
    suppose
      n in dom X;
      hence thesis by FINSEQ_2:11;
    end;
  end;
end;

definition
  let A be set;
  let X be FinSequence of bool A;
  redefine func Union X -> Subset of A;
  coherence
  proof
    union rng X c= A
    proof
      let x be set;
      assume x in union rng X;
      then ex Y being set st x in Y & Y in rng X by TARSKI:def 4;
      hence thesis;
    end;
    hence thesis;
  end;
end;

registration
  let A be finite set;
  let R be Relation of A;
  cluster RelStr (# A, R #) -> finite;
  coherence;
end;

theorem Th7:
  for X, x, y being set, T being Tolerance of X st x in Class (T, y
  ) holds y in Class (T, x)
proof
  let X, x, y be set, T be Tolerance of X;
  assume x in Class (T, y);
  then [x,y] in T by EQREL_1:19;
  then [y,x] in T by EQREL_1:6;
  hence thesis by EQREL_1:19;
end;

begin :: Tolerance and Approximation Spaces

definition
  let P be RelStr;
  attr P is with_equivalence means
  :Def2:
  the InternalRel of P is Equivalence_Relation of the carrier of P;
  attr P is with_tolerance means
  :Def3:
  the InternalRel of P is Tolerance of the carrier of P;
end;

registration
  cluster with_equivalence -> with_tolerance for RelStr;
  coherence
  proof
    let L be RelStr;
    assume L is with_equivalence;
    then
    the InternalRel of L is Equivalence_Relation of the carrier of L by Def2;
    hence thesis by Def3;
  end;
end;

registration
  let A be set;
  cluster RelStr (# A, id A #) -> with_equivalence;
  coherence by Def2;
end;

registration
  cluster discrete finite with_equivalence non empty for RelStr;
  existence
  proof
    set E = RelStr (# {{}}, id {{}} #);
    E is discrete;
    hence thesis;
  end;
  cluster non diagonal finite with_equivalence non empty for RelStr;
  existence
  proof
    set C = {0,1};
    set R = Total C;
    set E = RelStr (# C, R #);
    reconsider E as non empty RelStr;
    E is with_equivalence & C is non trivial by Def2,CHAIN_1:3;
    hence thesis;
  end;
end;

definition
  mode Approximation_Space is with_equivalence non empty RelStr;
  mode Tolerance_Space is with_tolerance non empty RelStr;
end;

registration
  let A be Tolerance_Space;
  cluster the InternalRel of A -> total reflexive symmetric;
  coherence by Def3;
end;

registration
  let A be Approximation_Space;
  cluster the InternalRel of A -> transitive;
  coherence by Def2;
end;

definition
  let A be non empty RelStr;
  let X be Subset of A;
  func LAp X -> Subset of A equals
  { x where x is Element of A : Class (the
  InternalRel of A, x) c= X };
  coherence
  proof
    { x where x is Element of A : Class (the InternalRel of A, x) c= X }
    c= the carrier of A
    proof
      let y be set;
      assume y in { x where x is Element of A : Class (the InternalRel of A,
      x) c= X };
      then
      ex x being Element of A st y = x & Class (the InternalRel of A, x) c= X;
      hence thesis;
    end;
    hence thesis;
  end;
  func UAp X -> Subset of A equals
  { x where x is Element of A : Class (the
  InternalRel of A, x) meets X };
  coherence
  proof
    { x where x is Element of A : Class (the InternalRel of A, x) meets X
    } c= the carrier of A
    proof
      let y be set;
      assume y in { x where x is Element of A : Class (the InternalRel of A,
      x) meets X };
      then ex x being Element of A st y = x & Class (the InternalRel of A, x)
      meets X;
      hence thesis;
    end;
    hence thesis;
  end;
end;

definition
  let A be non empty RelStr;
  let X be Subset of A;
  func BndAp X -> Subset of A equals
  UAp X \ LAp X;
  coherence;
end;

definition
  let A be non empty RelStr;
  let X be Subset of A;
  attr X is rough means
  :Def7:
  BndAp X <> {};
end;

notation
  let A be non empty RelStr;
  let X be Subset of A;
  antonym X is exact for X is rough;
end;

reserve A for Tolerance_Space,
  X, Y for Subset of A;

theorem Th8:
  for x being set st x in LAp X holds Class (the InternalRel of A, x) c= X
proof
  let x be set;
  assume x in LAp X;
  then
  ex x1 being Element of A st x = x1 & Class (the InternalRel of A, x1) c= X;
  hence thesis;
end;

theorem
  for x being Element of A st Class (the InternalRel of A, x) c= X holds
  x in LAp X;

theorem Th10:
  for x being set st x in UAp X holds Class (the InternalRel of A, x) meets X
proof
  let x be set;
  assume x in UAp X;
  then ex x1 being Element of A st x = x1 & Class (the InternalRel of A, x1)
  meets X;
  hence thesis;
end;

theorem
  for x being Element of A st Class (the InternalRel of A, x) meets X
  holds x in UAp X;

theorem Th12:
  LAp X c= X
proof
  let x be set;
  assume x in LAp X;
  then consider y being Element of A such that
A1: y = x & Class (the InternalRel of A, y) c= X;
  y in Class (the InternalRel of A, y) by EQREL_1:20;
  hence thesis by A1;
end;

theorem Th13:
  X c= UAp X
proof
  let x be set;
  assume
A1: x in X;
  then reconsider x9 = x as Element of A;
  x9 in Class (the InternalRel of A, x9) by EQREL_1:20;
  then Class (the InternalRel of A, x9) meets X by A1,XBOOLE_0:3;
  hence thesis;
end;

theorem Th14:
  LAp X c= UAp X
proof
  LAp X c= X & X c= UAp X by Th12,Th13;
  hence thesis by XBOOLE_1:1;
end;

theorem Th15:
  X is exact iff LAp X = X
proof
A1: LAp X c= UAp X by Th14;
  hereby
    assume X is exact;
    then BndAp X = {} by Def7;
    then UAp X c= LAp X by XBOOLE_1:37;
    then UAp X = LAp X by A1,XBOOLE_0:def 10;
    then
A2: X c= LAp X by Th13;
    LAp X c= X by Th12;
    hence LAp X = X by A2,XBOOLE_0:def 10;
  end;
  assume
A3: LAp X = X;
  UAp X c= X
  proof
    let y be set;
    assume y in UAp X;
    then Class (the InternalRel of A, y) meets X by Th10;
    then consider z being set such that
A4: z in Class (the InternalRel of A, y) & z in LAp X by A3,XBOOLE_0:3;
    Class (the InternalRel of A, z) c= X & y in Class (the InternalRel of
    A, z) by A4,Th7,Th8;
    hence thesis;
  end;
  then BndAp X = {} by A3,XBOOLE_1:37;
  hence thesis by Def7;
end;

theorem Th16:
  X is exact iff UAp X = X
proof
  hereby
    assume X is exact;
    then BndAp X = {} by Def7;
    then
A1: UAp X c= LAp X by XBOOLE_1:37;
A2: X c= UAp X by Th13;
    LAp X c= X by Th12;
    then UAp X c= X by A1,XBOOLE_1:1;
    hence UAp X = X by A2,XBOOLE_0:def 10;
  end;
  assume
A3: UAp X = X;
  X c= LAp X
  proof
    let x be set;
    assume
A4: x in X;
    Class (the InternalRel of A, x) c= X
    proof
      let y be set;
      assume
A5:   y in Class (the InternalRel of A, x);
      then [y,x] in the InternalRel of A by EQREL_1:19;
      then [x,y] in the InternalRel of A by EQREL_1:6;
      then x in Class (the InternalRel of A, y) by EQREL_1:19;
      then Class (the InternalRel of A, y) meets X by A4,XBOOLE_0:3;
      hence thesis by A3,A5;
    end;
    hence thesis by A4;
  end;
  then BndAp X = {} by A3,XBOOLE_1:37;
  hence thesis by Def7;
end;

theorem
  X = LAp X iff X = UAp X
proof
  X = LAp X iff X is exact by Th15;
  hence thesis by Th16;
end;

theorem Th18:
  LAp {}A = {}
proof
  assume LAp {}A <> {};
  then consider x being set such that
A1: x in LAp {}A by XBOOLE_0:def 1;
  ex y being Element of A st y = x & Class (the InternalRel of A, y) c= {}A
  by A1;
  hence thesis by EQREL_1:20;
end;

theorem Th19:
  UAp {}A = {}
proof
  assume UAp {}A <> {};
  then consider x being set such that
A1: x in UAp {}A by XBOOLE_0:def 1;
  ex y being Element of A st y = x & Class (the InternalRel of A, y) meets
  {}A by A1;
  hence thesis by XBOOLE_1:65;
end;

theorem Th20:
  LAp [#]A = [#]A
proof
  thus LAp [#]A c= [#]A;
  let x be set;
A1: Class (the InternalRel of A, x) c= [#]A;
  assume x in [#]A;
  hence thesis by A1;
end;

theorem
  UAp [#]A = [#]A
proof
  LAp [#]A c= UAp [#]A by Th14;
  then [#]A c= UAp [#]A by Th20;
  hence thesis by XBOOLE_0:def 10;
end;

theorem
  LAp (X /\ Y) = LAp X /\ LAp Y
proof
  thus LAp (X /\ Y) c= LAp X /\ LAp Y
  proof
    let x be set;
    assume
A1: x in LAp (X /\ Y);
    then Class (the InternalRel of A, x) c= Y by Th8,XBOOLE_1:18;
    then
A2: x in LAp Y by A1;
    Class (the InternalRel of A, x) c= X by A1,Th8,XBOOLE_1:18;
    then x in LAp X by A1;
    hence thesis by A2,XBOOLE_0:def 4;
  end;
  let x be set;
  assume
A3: x in LAp X /\ LAp Y;
  then x in LAp Y by XBOOLE_0:def 4;
  then
A4: Class (the InternalRel of A, x) c= Y by Th8;
  x in LAp X by A3,XBOOLE_0:def 4;
  then Class (the InternalRel of A, x) c= X by Th8;
  then Class (the InternalRel of A, x) c= X /\ Y by A4,XBOOLE_1:19;
  hence thesis by A3;
end;

theorem
  UAp (X \/ Y) = UAp X \/ UAp Y
proof
  thus UAp (X \/ Y) c= UAp X \/ UAp Y
  proof
    let x be set;
    assume
A1: x in UAp (X \/ Y);
    then Class (the InternalRel of A, x) meets (X \/ Y) by Th10;
    then
    Class (the InternalRel of A, x) meets X or Class (the InternalRel of A
    , x) meets Y by XBOOLE_1:70;
    then x in UAp X or x in UAp Y by A1;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be set;
  assume
A2: x in UAp X \/ UAp Y;
  then x in UAp X or x in UAp Y by XBOOLE_0:def 3;
  then
  Class (the InternalRel of A, x) meets X or Class (the InternalRel of A,
  x) meets Y by Th10;
  then Class (the InternalRel of A, x) meets (X \/ Y) by XBOOLE_1:70;
  hence thesis by A2;
end;

theorem Th24:
  X c= Y implies LAp X c= LAp Y
proof
  assume
A1: X c= Y;
  let x be set;
  assume
A2: x in LAp X;
  then Class (the InternalRel of A, x) c= X by Th8;
  then Class (the InternalRel of A, x) c= Y by A1,XBOOLE_1:1;
  hence thesis by A2;
end;

theorem Th25:
  X c= Y implies UAp X c= UAp Y
proof
  assume
A1: X c= Y;
  let x be set;
  assume
A2: x in UAp X;
  then Class (the InternalRel of A, x) meets X by Th10;
  then Class (the InternalRel of A, x) meets Y by A1,XBOOLE_1:63;
  hence thesis by A2;
end;

theorem
  LAp X \/ LAp Y c= LAp (X \/ Y)
proof
  let x be set;
  assume
A1: x in LAp X \/ LAp Y;
  per cases by A1,XBOOLE_0:def 3;
  suppose
    x in LAp X;
    then Class (the InternalRel of A, x) c= X \/ Y by Th8,XBOOLE_1:10;
    hence thesis by A1;
  end;
  suppose
    x in LAp Y;
    then Class (the InternalRel of A, x) c= X \/ Y by Th8,XBOOLE_1:10;
    hence thesis by A1;
  end;
end;

theorem
  UAp (X /\ Y) c= UAp X /\ UAp Y
proof
  let x be set;
  assume
A1: x in UAp (X /\ Y);
  then Class (the InternalRel of A, x) meets Y by Th10,XBOOLE_1:74;
  then
A2: x in UAp Y by A1;
  Class (the InternalRel of A, x) meets X by A1,Th10,XBOOLE_1:74;
  then x in UAp X by A1;
  hence thesis by A2,XBOOLE_0:def 4;
end;

theorem Th28:
  LAp X` = (UAp X)`
proof
  LAp X` misses UAp X
  proof
    assume LAp X` meets UAp X;
    then consider x being set such that
A1: x in LAp X` & x in UAp X by XBOOLE_0:3;
    Class (the InternalRel of A, x) meets X & Class (the InternalRel of A,
    x) c= X` by A1,Th8,Th10;
    hence thesis by XBOOLE_1:63,79;
  end;
  hence LAp X` c= (UAp X)` by SUBSET_1:23;
  let x be set;
  assume
A2: x in (UAp X)`;
  then not x in UAp X by XBOOLE_0:def 5;
  then Class (the InternalRel of A, x) misses X by A2;
  then Class (the InternalRel of A, x) c= X` by SUBSET_1:23;
  hence thesis by A2;
end;

theorem Th29:
  UAp X` = (LAp X)`
proof
  (UAp X`)`` = (LAp X``)` by Th28;
  hence thesis;
end;

theorem
  UAp LAp UAp X = UAp X
proof
  thus UAp LAp UAp X c= UAp X
  proof
    let x be set;
    assume x in UAp LAp UAp X;
    then Class (the InternalRel of A, x) meets LAp UAp X by Th10;
    then consider y being set such that
A1: y in Class (the InternalRel of A, x) and
A2: y in LAp UAp X by XBOOLE_0:3;
    [y, x] in the InternalRel of A by A1,EQREL_1:19;
    then [x, y] in the InternalRel of A by EQREL_1:6;
    then
A3: x in Class (the InternalRel of A, y) by EQREL_1:19;
    Class (the InternalRel of A, y) c= UAp X by A2,Th8;
    hence thesis by A3;
  end;
  X c= LAp UAp X
  proof
    let x be set;
    assume
A4: x in X;
    Class (the InternalRel of A, x) c= UAp X
    proof
      let y be set;
      assume
A5:   y in Class (the InternalRel of A, x);
      then [y,x] in the InternalRel of A by EQREL_1:19;
      then [x,y] in the InternalRel of A by EQREL_1:6;
      then x in Class (the InternalRel of A, y) by EQREL_1:19;
      then Class (the InternalRel of A, y) meets X by A4,XBOOLE_0:3;
      hence thesis by A5;
    end;
    hence thesis by A4;
  end;
  hence UAp X c= UAp LAp UAp X by Th25;
end;

theorem
  LAp UAp LAp X = LAp X
proof
  UAp LAp X c= X
  proof
    let y be set;
    assume y in UAp LAp X;
    then Class (the InternalRel of A, y) meets LAp X by Th10;
    then consider z being set such that
A1: z in Class (the InternalRel of A, y) and
A2: z in LAp X by XBOOLE_0:3;
    [z,y] in the InternalRel of A by A1,EQREL_1:19;
    then [y,z] in the InternalRel of A by EQREL_1:6;
    then
A3: y in Class (the InternalRel of A, z) by EQREL_1:19;
    Class (the InternalRel of A, z) c= X by A2,Th8;
    hence thesis by A3;
  end;
  hence LAp UAp LAp X c= LAp X by Th24;
  thus LAp X c= LAp UAp LAp X
  proof
    let x be set;
    assume
A4: x in LAp X;
    Class (the InternalRel of A, x) c= UAp LAp X
    proof
      let y be set;
      assume
A5:   y in Class (the InternalRel of A, x);
      then [y,x] in the InternalRel of A by EQREL_1:19;
      then [x,y] in the InternalRel of A by EQREL_1:6;
      then x in Class (the InternalRel of A, y) by EQREL_1:19;
      then Class (the InternalRel of A, y) meets LAp X by A4,XBOOLE_0:3;
      hence thesis by A5;
    end;
    hence thesis by A4;
  end;
end;

theorem
  BndAp X = BndAp X`
proof
  thus BndAp X c= BndAp X`
  proof
    let x be set;
    assume
A1: x in BndAp X;
    then x in UAp X by XBOOLE_0:def 5;
    then not x in (UAp X)` by XBOOLE_0:def 5;
    then
A2: not x in LAp X` by Th28;
    not x in LAp X by A1,XBOOLE_0:def 5;
    then x in (LAp X)` by A1,XBOOLE_0:def 5;
    then x in UAp X` by Th29;
    hence thesis by A2,XBOOLE_0:def 5;
  end;
  thus BndAp X` c= BndAp X
  proof
    let x be set;
    assume
A3: x in BndAp X`;
    then x in UAp X` by XBOOLE_0:def 5;
    then x in (LAp X)` by Th29;
    then
A4: not x in LAp X by XBOOLE_0:def 5;
    not x in LAp X` by A3,XBOOLE_0:def 5;
    then not x in (UAp X)` by Th28;
    then x in (UAp X)`` by A3,SUBSET_1:29;
    hence thesis by A4,XBOOLE_0:def 5;
  end;
end;

reserve A for Approximation_Space,
  X for Subset of A;

theorem
  LAp LAp X = LAp X
proof
  thus LAp LAp X c= LAp X by Th12;
  let x be set;
  assume
A1: x in LAp X;
  then
A2: Class (the InternalRel of A, x) c= X by Th8;
  Class (the InternalRel of A, x) c= LAp X
  proof
    let y be set;
    assume
A3: y in Class (the InternalRel of A, x);
    then Class (the InternalRel of A, x) = Class (the InternalRel of A, y) by
A1,EQREL_1:23;
    hence thesis by A2,A3;
  end;
  hence thesis by A1;
end;

theorem Th34:
  LAp LAp X = UAp LAp X
proof
  thus LAp LAp X c= UAp LAp X by Th14;
  let x be set;
  assume
A1: x in UAp LAp X;
  then Class (the InternalRel of A, x) meets LAp X by Th10;
  then consider z being set such that
A2: z in Class (the InternalRel of A, x) and
A3: z in LAp X by XBOOLE_0:3;
  Class (the InternalRel of A, z) c= X by A3,Th8;
  then
A4: Class (the InternalRel of A, x) c= X by A1,A2,EQREL_1:23;
  Class (the InternalRel of A, x) c= LAp X
  proof
    let y be set;
    assume
A5: y in Class (the InternalRel of A, x);
    then Class (the InternalRel of A, x) = Class (the InternalRel of A, y) by
A1,EQREL_1:23;
    hence thesis by A4,A5;
  end;
  hence thesis by A1;
end;

theorem
  UAp UAp X = UAp X
proof
  hereby
    let x be set;
    assume
A1: x in UAp UAp X;
    then Class (the InternalRel of A, x) meets UAp X by Th10;
    then consider y being set such that
A2: y in Class (the InternalRel of A, x) and
A3: y in UAp X by XBOOLE_0:3;
A4: Class (the InternalRel of A, y) = Class (the InternalRel of A, x) by A1,A2,
EQREL_1:23;
    Class (the InternalRel of A, y) meets X by A3,Th10;
    hence x in UAp X by A1,A4;
  end;
  thus thesis by Th13;
end;

theorem Th36:
  UAp UAp X = LAp UAp X
proof
  thus UAp UAp X c= LAp UAp X
  proof
    let x be set;
    assume
A1: x in UAp UAp X;
    then Class (the InternalRel of A, x) meets UAp X by Th10;
    then consider z being set such that
A2: z in Class (the InternalRel of A, x) and
A3: z in UAp X by XBOOLE_0:3;
A4: Class (the InternalRel of A, z) = Class (the InternalRel of A, x) by A1,A2,
EQREL_1:23;
A5: Class (the InternalRel of A, z) meets X by A3,Th10;
    Class (the InternalRel of A, x) c= UAp X
    proof
      let y be set;
      assume
A6:   y in Class (the InternalRel of A, x);
      then
      Class (the InternalRel of A, x) = Class (the InternalRel of A, y) by A1,
EQREL_1:23;
      hence thesis by A5,A4,A6;
    end;
    hence thesis by A1;
  end;
  thus thesis by Th14;
end;

registration
  let A be Tolerance_Space;
  cluster exact for Subset of A;
  existence
  proof
    take {}A;
    LAp {}A = {} by Th18;
    hence thesis by Th15;
  end;
end;

registration
  let A be Approximation_Space;
  let X be Subset of A;
  cluster LAp X -> exact;
  coherence
  proof
    set Y = LAp X;
    UAp Y = LAp Y by Th34;
    then BndAp Y = {} by XBOOLE_1:37;
    hence thesis by Def7;
  end;
  cluster UAp X -> exact;
  coherence
  proof
    set Y = UAp X;
    UAp Y = LAp Y by Th36;
    then BndAp Y = {} by XBOOLE_1:37;
    hence thesis by Def7;
  end;
end;

theorem Th37:
  for A being Approximation_Space, X being Subset of A, x, y being
  set st x in UAp X & [x,y] in the InternalRel of A holds y in UAp X
proof
  let A be Approximation_Space, X be Subset of A;
  let x, y be set;
  assume that
A1: x in UAp X and
A2: [x,y] in the InternalRel of A;
  [y,x] in the InternalRel of A by A2,EQREL_1:6;
  then y in Class (the InternalRel of A, x) by EQREL_1:19;
  then
A3: Class (the InternalRel of A, x) = Class (the InternalRel of A, y) by A1,
EQREL_1:23;
  Class (the InternalRel of A, x) meets X & y is Element of A by A1,A2,Th10,
ZFMISC_1:87;
  hence thesis by A3;
end;

registration
  let A be non diagonal Approximation_Space;
  cluster rough for Subset of A;
  existence
  proof
    consider x, y being Element of A such that
A1: x <> y and
A2: [x,y] in the InternalRel of A by Th4;
    set X = {x};
    x in X & X c= UAp X by Th13,TARSKI:def 1;
    then y in UAp X by A2,Th37;
    then UAp X <> X by A1,TARSKI:def 1;
    then X is not exact by Th16;
    hence thesis;
  end;
end;

definition
  let A be Approximation_Space;
  let X be Subset of A;
  mode RoughSet of X means
    it = [LAp X, UAp X];
  existence;
end;

begin :: Membership Function

registration
  let A be finite Tolerance_Space, x be Element of A;
  cluster card Class (the InternalRel of A, x) -> non empty;
  coherence
  proof
    x in Class (the InternalRel of A, x) by EQREL_1:20;
    hence thesis;
  end;
end;

definition
  let A be finite Tolerance_Space;
  let X be Subset of A;
  func MemberFunc (X, A) -> Function of the carrier of A, REAL means
  :Def9:
for x being Element of A holds it.x = card (X /\ Class (the InternalRel of A, x
  )) / (card Class (the InternalRel of A, x));
  existence
  proof
    deffunc F(set) = card (X /\ Class (the InternalRel of A, $1)) / (card
    Class (the InternalRel of A, $1));
A1: for x being set st x in the carrier of A holds F(x) in REAL by
XREAL_0:def 1;
    ex f being Function of the carrier of A, REAL st for x being set st x
    in the carrier of A holds f.x = F(x) from FUNCT_2:sch 2(A1);
    then consider f being Function of the carrier of A, REAL such that
A2: for x being set st x in the carrier of A holds f.x = F(x);
    take f;
    let x be Element of A;
    thus thesis by A2;
  end;
  uniqueness
  proof
    deffunc F(Element of A) = card (X /\ Class (the InternalRel of A, $1)) / (
    card Class (the InternalRel of A, $1));
A3: for A1,A2 being Function of the carrier of A, REAL st (for x being
Element of A holds A1.x = F(x)) & (for x being Element of A holds A2.x = F(x))
    holds A1 = A2 from BINOP_2:sch 1;
    let A1, A2 be Function of the carrier of A, REAL;
    assume ( for x being Element of A holds A1.x = F(x))& for x being Element
    of A holds A2.x = F(x);
    hence A1 = A2 by A3;
  end;
end;

reserve A for finite Tolerance_Space,
  X for Subset of A,
  x for Element of A;

theorem Th38:
  0 <= MemberFunc (X, A).x & MemberFunc (X, A).x <= 1
proof
  card (X /\ Class (the InternalRel of A, x)) / (card Class (the
  InternalRel of A, x)) >= 0;
  hence 0 <= MemberFunc (X, A).x by Def9;
  card (X /\ Class (the InternalRel of A, x)) <= (card Class (the
  InternalRel of A, x)) by NAT_1:43,XBOOLE_1:17;
  then card (X /\ Class (the InternalRel of A, x)) / (card Class (the
  InternalRel of A, x)) <= 1 by XREAL_1:185;
  hence thesis by Def9;
end;

theorem
  MemberFunc (X, A).x in [. 0, 1 .]
proof
  0 <= MemberFunc (X, A).x & MemberFunc (X, A).x <= 1 by Th38;
  hence thesis by XXREAL_1:1;
end;

reserve A for finite Approximation_Space,
  X, Y for Subset of A,
  x for Element of A;

theorem Th40:
  MemberFunc (X, A).x = 1 iff x in LAp X
proof
  hereby
    assume
A1: MemberFunc (X, A).x = 1;
    MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (
    card Class (the InternalRel of A, x)) by Def9;
    then card (X /\ Class (the InternalRel of A, x)) = (card Class (the
    InternalRel of A, x)) by A1,XCMPLX_1:58;
    then
    X /\ Class (the InternalRel of A, x) = Class (the InternalRel of A, x)
    by PRE_POLY:8,XBOOLE_1:17;
    then Class (the InternalRel of A, x) c= X by XBOOLE_1:18;
    hence x in LAp X;
  end;
  assume x in LAp X;
  then
A2: card (X /\ Class (the InternalRel of A, x)) = card Class (the
  InternalRel of A, x) by Th8,XBOOLE_1:28;
  MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (
  card Class (the InternalRel of A, x)) by Def9;
  hence thesis by A2,XCMPLX_1:60;
end;

theorem Th41:
  MemberFunc (X, A).x = 0 iff x in (UAp X)`
proof
  hereby
    assume
A1: MemberFunc (X, A).x = 0;
    MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (
    card Class (the InternalRel of A, x)) by Def9;
    then X /\ Class (the InternalRel of A, x) = {} by A1,XCMPLX_1:50;
    then X misses Class (the InternalRel of A, x) by XBOOLE_0:def 7;
    then not x in UAp X by Th10;
    hence x in (UAp X)` by XBOOLE_0:def 5;
  end;
  assume x in (UAp X)`;
  then not x in UAp X by XBOOLE_0:def 5;
  then X misses Class (the InternalRel of A, x);
  then
A2: card (X /\ Class (the InternalRel of A, x)) = 0 by CARD_1:27,XBOOLE_0:def 7
;
  MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (
  card Class (the InternalRel of A, x)) by Def9;
  hence thesis by A2;
end;

theorem Th42:
  0 < MemberFunc (X, A).x & MemberFunc (X, A).x < 1 iff x in BndAp X
proof
  hereby
    assume that
A1: 0 < MemberFunc (X, A).x and
A2: MemberFunc (X, A).x < 1;
    not x in (UAp X)` by A1,Th41;
    then
A3: x in UAp X by XBOOLE_0:def 5;
    not x in LAp X by A2,Th40;
    hence x in BndAp X by A3,XBOOLE_0:def 5;
  end;
  assume
A4: x in BndAp X;
  then not x in LAp X by XBOOLE_0:def 5;
  then
A5: MemberFunc (X, A).x <> 1 by Th40;
  x in UAp X by A4,XBOOLE_0:def 5;
  then not x in (UAp X)` by XBOOLE_0:def 5;
  then
A6: 0 <> MemberFunc (X, A).x by Th41;
  MemberFunc (X, A).x <= 1 by Th38;
  hence thesis by A6,A5,Th38,XXREAL_0:1;
end;

theorem Th43:
  for A being discrete Approximation_Space, X being Subset of A
  holds X is exact
proof
  let A be discrete Approximation_Space, X be Subset of A;
A1: the InternalRel of A = id the carrier of A by ORDERS_3:def 1;
  X = UAp X
  proof
    thus X c= UAp X by Th13;
    let x be set;
    assume
A2: x in UAp X;
    then Class (the InternalRel of A, x) meets X by Th10;
    then
A3: ex y being set st y in Class (the InternalRel of A, x) & y in X by
XBOOLE_0:3;
    Class (the InternalRel of A, x) = {x} by A1,A2,EQREL_1:25;
    hence thesis by A3,TARSKI:def 1;
  end;
  hence thesis;
end;

registration
  let A be discrete Approximation_Space;
  cluster -> exact for Subset of A;
  coherence by Th43;
end;

theorem
  for A being discrete finite Approximation_Space, X being Subset of A
  holds MemberFunc (X, A) = chi (X, the carrier of A)
proof
  let A be discrete finite Approximation_Space, X be Subset of A;
  reconsider F = MemberFunc (X, A) as Function of the carrier of A, REAL;
  set G = chi (X, the carrier of A);
  {0,1 qua Element of REAL} c= REAL;
  then reconsider G as Function of the carrier of A, REAL by FUNCT_2:7;
  for x being set st x in the carrier of A holds F.x = G.x
  proof
    let x be set;
    assume
A1: x in the carrier of A;
    per cases;
    suppose
A2:   x in X;
      then x in LAp X by Th15;
      then F.x = 1 by Th40;
      hence thesis by A2,FUNCT_3:def 3;
    end;
    suppose
A3:   not x in X;
      then not x in UAp X by Th16;
      then x in (UAp X)` by A1,XBOOLE_0:def 5;
      then F.x = 0 by Th41;
      hence thesis by A1,A3,FUNCT_3:def 3;
    end;
  end;
  hence thesis by FUNCT_2:12;
end;

theorem
  for A being finite Approximation_Space, X being Subset of A, x, y
  being set st [x,y] in the InternalRel of A holds MemberFunc (X, A).x =
  MemberFunc (X, A).y
proof
  let A be finite Approximation_Space, X be Subset of A, x, y be set;
  assume
A1: [x,y] in the InternalRel of A;
  then
A2: y is Element of A by ZFMISC_1:87;
  x is Element of A by A1,ZFMISC_1:87;
  then
A3: MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (
  card Class (the InternalRel of A, x)) by Def9;
  x in Class (the InternalRel of A, y) by A1,EQREL_1:19;
  then
  Class (the InternalRel of A, x) = Class (the InternalRel of A, y) by A2,
EQREL_1:23;
  hence thesis by A2,A3,Def9;
end;

theorem
  MemberFunc (X`,A).x = 1 - (MemberFunc (X,A).x)
proof
A1: [#]A /\ Class (the InternalRel of A, x) = Class (the InternalRel of A, x
  ) by XBOOLE_1:28;
  MemberFunc (X`,A).x = card (([#]A \ X) /\ Class (the InternalRel of A, x
  )) / (card Class (the InternalRel of A, x)) by Def9
    .= (card (([#]A /\ Class (the InternalRel of A, x)) \ (X /\ Class (the
InternalRel of A, x)))) / (card Class (the InternalRel of A, x)) by XBOOLE_1:50
    .= (card ([#]A /\ Class (the InternalRel of A, x)) - card (X /\ Class (
  the InternalRel of A, x))) / (card Class (the InternalRel of A, x)) by A1,
CARD_2:44,XBOOLE_1:17
    .= card ([#]A /\ Class (the InternalRel of A, x))/ (card Class (the
  InternalRel of A, x)) - (card (X /\ Class (the InternalRel of A, x)) / (card
  Class (the InternalRel of A, x))) by XCMPLX_1:120
    .= card (Class (the InternalRel of A, x))/ (card Class (the InternalRel
  of A, x)) - (card (X /\ Class (the InternalRel of A, x)) / (card Class (the
  InternalRel of A, x))) by XBOOLE_1:28
    .= 1 - card (X /\ Class (the InternalRel of A, x)) / (card Class (the
  InternalRel of A, x)) by XCMPLX_1:60
    .= 1 - (MemberFunc (X,A).x) by Def9;
  hence thesis;
end;

theorem Th47:
  X c= Y implies MemberFunc (X, A).x <= MemberFunc (Y, A).x
proof
  set CI = Class (the InternalRel of A, x);
  assume X c= Y;
  then card (Y /\ CI) >= card (X /\ CI) by NAT_1:43,XBOOLE_1:26;
  then
A1: card (Y /\ CI) / (card CI) >= card (X /\ CI) / (card CI) by XREAL_1:72;
  MemberFunc (X, A).x = card (X /\ CI) / (card CI) by Def9;
  hence thesis by A1,Def9;
end;

theorem
  MemberFunc (X \/ Y, A).x >= MemberFunc (X, A).x by Th47,XBOOLE_1:7;

theorem
  MemberFunc (X /\ Y, A).x <= MemberFunc (X, A).x by Th47,XBOOLE_1:17;

theorem
  MemberFunc (X \/ Y, A).x >= max (MemberFunc (X, A).x, MemberFunc (Y, A ).x)
proof
  MemberFunc (X \/ Y, A).x >= MemberFunc (X, A).x & MemberFunc (X \/ Y, A)
  .x >= MemberFunc (Y, A).x by Th47,XBOOLE_1:7;
  hence thesis by XXREAL_0:28;
end;

theorem Th51:
  X misses Y implies MemberFunc (X \/ Y, A).x = MemberFunc (X, A).
  x + MemberFunc (Y, A).x
proof
  assume
A1: X misses Y;
  card ((X \/ Y) /\ Class (the InternalRel of A, x)) = card ((X /\ Class (
  the InternalRel of A, x)) \/ (Y /\ Class (the InternalRel of A, x))) by
XBOOLE_1:23
    .= card (X /\ Class (the InternalRel of A, x)) + card (Y /\ Class (the
  InternalRel of A, x)) by A1,CARD_2:40,XBOOLE_1:76;
  then
  MemberFunc (X \/ Y, A).x = (card (X /\ Class (the InternalRel of A, x))
  + card (Y /\ Class (the InternalRel of A, x))) / (card Class (the InternalRel
  of A, x)) by Def9
    .= card (X /\ Class (the InternalRel of A, x)) / (card Class (the
  InternalRel of A, x)) + card (Y /\ Class (the InternalRel of A, x)) / (card
  Class (the InternalRel of A, x)) by XCMPLX_1:62
    .= MemberFunc (X, A).x + card (Y /\ Class (the InternalRel of A, x)) / (
  card Class (the InternalRel of A, x)) by Def9
    .= MemberFunc (X, A).x + MemberFunc (Y, A).x by Def9;
  hence thesis;
end;

theorem
  MemberFunc (X /\ Y, A).x <= min (MemberFunc (X, A).x, MemberFunc (Y, A ).x)
proof
  MemberFunc (X /\ Y, A).x <= MemberFunc (X, A).x & MemberFunc (X /\ Y, A)
  .x <= MemberFunc (Y, A).x by Th47,XBOOLE_1:17;
  hence thesis by XXREAL_0:20;
end;

definition
  let A be finite Tolerance_Space;
  let X be FinSequence of bool the carrier of A;
  let x be Element of A;
  func FinSeqM (x,X) -> FinSequence of REAL means
  :Def10:
  dom it = dom X & for
  n being Nat st n in dom X holds it.n = MemberFunc (X.n, A).x;
  existence
  proof
    deffunc F(Nat) = MemberFunc (X.$1, A).x;
    ex z being FinSequence of REAL st len z = len X & for j being Nat st j
    in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
    then consider z being FinSequence of REAL such that
A1: len z = len X and
A2: for j being Nat st j in dom z holds z.j = F(j);
    take z;
    thus dom z = Seg len z by FINSEQ_1:def 3
      .= dom X by A1,FINSEQ_1:def 3;
    let n be Nat;
    assume n in dom X;
    then
A3: n in Seg len X by FINSEQ_1:def 3;
    dom z = Seg len X by A1,FINSEQ_1:def 3;
    hence thesis by A2,A3;
  end;
  uniqueness
  proof
    let A1, A2 be FinSequence of REAL such that
A4: dom A1 = dom X and
A5: for n being Nat st n in dom X holds A1.n = MemberFunc (X.n, A).x and
A6: dom A2 = dom X and
A7: for n being Nat st n in dom X holds A2.n = MemberFunc (X.n, A).x;
    for n being Nat st n in dom A1 holds A1.n = A2.n
    proof
      let n be Nat;
      assume
A8:   n in dom A1;
      reconsider n as Element of NAT by ORDINAL1:def 12;
      A1.n = MemberFunc (X.n, A).x by A4,A5,A8
        .= A2.n by A4,A7,A8;
      hence thesis;
    end;
    hence thesis by A4,A6,FINSEQ_1:13;
  end;
end;

theorem Th53:
  for X being FinSequence of bool the carrier of A, x being
Element of A, y being Subset of A holds FinSeqM (x, X^<*y*>) = FinSeqM (x, X) ^
  <* MemberFunc (y, A).x *>
proof
  let X be FinSequence of bool the carrier of A, x be Element of A, y be
  Subset of A;
  set p = FinSeqM (x, X^<*y*>);
  set q = FinSeqM (x, X) ^ <* MemberFunc (y, A).x *>;
  dom X = dom FinSeqM (x, X) by Def10;
  then Seg len X = dom FinSeqM (x, X) by FINSEQ_1:def 3
    .= Seg len FinSeqM (x, X) by FINSEQ_1:def 3;
  then
A1: len X = len FinSeqM (x, X) by FINSEQ_1:6;
A2: dom p = dom (X^<*y*>) by Def10
    .= Seg (len X + len <* y *>) by FINSEQ_1:def 7
    .= Seg (len X + 1) by FINSEQ_1:39;
A3: for k being Nat st k in dom p holds p.k = q.k
  proof
    let k be Nat;
    assume
A4: k in dom p;
    then reconsider k as Element of NAT;
A5: 1 <= k by A4,FINSEQ_3:25;
    k in dom (X^<*y*>) by A4,Def10;
    then
A6: p.k = MemberFunc ((X^<*y*>).k, A).x by Def10;
A7: k <= len X + 1 by A2,A4,FINSEQ_1:1;
    per cases by A7,NAT_1:8;
    suppose
A8:   k <= len X;
      then
A9:   k in dom X by A5,FINSEQ_3:25;
      k in dom FinSeqM (x, X) by A1,A5,A8,FINSEQ_3:25;
      then q.k = FinSeqM (x, X).k by FINSEQ_1:def 7
        .= MemberFunc (X.k, A).x by A9,Def10;
      hence thesis by A6,A9,FINSEQ_1:def 7;
    end;
    suppose
A10:  k = len X + 1;
      then q.k = MemberFunc (y, A).x by A1,FINSEQ_1:42;
      hence thesis by A6,A10,FINSEQ_1:42;
    end;
  end;
  dom q = Seg (len FinSeqM (x, X) + len <* MemberFunc (y, A).x *>) by
FINSEQ_1:def 7
    .= Seg (len X + 1) by A1,FINSEQ_1:39;
  hence thesis by A2,A3,FINSEQ_1:13;
end;

theorem Th54:
  MemberFunc ({}A, A).x = 0
proof
  UAp {}A = {} by Th19;
  then (UAp {}A)` = [#] A;
  hence thesis by Th41;
end;

theorem
  for X being disjoint_valued FinSequence of bool the carrier of A holds
  MemberFunc (Union X, A).x = Sum FinSeqM (x, X)
proof
  let X be disjoint_valued FinSequence of bool the carrier of A;
  defpred P[FinSequence of bool the carrier of A] means $1 is disjoint_valued
  implies MemberFunc (Union $1, A).x = Sum FinSeqM (x, $1);
A1: for p being FinSequence of bool the carrier of A for y being Subset of A
  st P[p] holds P[p^<*y*>]
  proof
    let p be FinSequence of bool the carrier of A;
    let y be Subset of A;
    assume
A2: P[p];
    P[p^<*y*>]
    proof
      assume
A3:   p^<*y*> is disjoint_valued;
A4:   Union p misses y
      proof
        assume Union p meets y;
        then consider x being set such that
A5:     x in Union p and
A6:     x in y by XBOOLE_0:3;
        consider X being set such that
A7:     x in X and
A8:     X in rng p by A5,TARSKI:def 4;
        consider m being set such that
A9:     m in dom p and
A10:    X = p.m by A8,FUNCT_1:def 3;
        reconsider m as Element of NAT by A9;
A11:    (p^<*y*>).m = p.m & m <= len p by A9,FINSEQ_1:def 7,FINSEQ_3:25;
A12:    (p^<*y*>).(len p + 1) = y & len p < len p + 1 by FINSEQ_1:42,NAT_1:13;
        p.m meets y by A6,A7,A10,XBOOLE_0:3;
        hence thesis by A3,A12,A11,PROB_2:def 2;
      end;
      Union (p^<*y*>) = Union p \/ Union <*y*> by Th5
        .= Union p \/ y by FINSEQ_3:135;
      then MemberFunc (Union (p^<*y*>), A).x = MemberFunc (Union p, A).x +
      MemberFunc (y, A).x by A4,Th51
        .= Sum (FinSeqM (x, p) ^ <* MemberFunc (y, A).x *>) by A2,A3,Th6,
FINSEQ_6:10,RVSUM_1:74
        .= Sum FinSeqM (x, p ^ <*y*>) by Th53;
      hence thesis;
    end;
    hence thesis;
  end;
A13: P[<*> bool the carrier of A]
  proof
    set F = FinSeqM (x, <*> bool the carrier of A);
    assume <*> bool the carrier of A is disjoint_valued;
    dom F = dom <*> bool the carrier of A by Def10;
    then
A14: Sum F = 0 by RELAT_1:41,RVSUM_1:72;
    Union <*> bool the carrier of A = {}A by ZFMISC_1:2;
    hence thesis by A14,Th54;
  end;
  for p being FinSequence of bool the carrier of A holds P[p] from
  FINSEQ_2:sch 2 (A13,A1);
  hence thesis;
end;

theorem
  LAp X = { x where x is Element of A : MemberFunc (X, A).x = 1 }
proof
  thus LAp X c= { x where x is Element of A : MemberFunc (X, A).x = 1 }
  proof
    let y be set;
    assume
A1: y in LAp X;
    then reconsider y9 = y as Element of A;
    MemberFunc (X, A).y9 = 1 by A1,Th40;
    hence thesis;
  end;
  let y be set;
  assume y in { x where x is Element of A : MemberFunc (X, A).x = 1 };
  then ex y9 being Element of A st y9 = y & MemberFunc (X, A). y9 = 1;
  hence thesis by Th40;
end;

theorem
  UAp X = { x where x is Element of A : MemberFunc (X, A).x > 0 }
proof
  thus UAp X c= { x where x is Element of A : MemberFunc (X, A).x > 0 }
  proof
    let y be set;
    assume
A1: y in UAp X;
    then reconsider y9 = y as Element of A;
    not y in (UAp X)` by A1,XBOOLE_0:def 5;
    then MemberFunc (X, A).y9 <> 0 by Th41;
    then MemberFunc (X, A).y9 > 0 by Th38;
    hence thesis;
  end;
  let y be set;
  assume y in { x where x is Element of A : MemberFunc (X, A).x > 0 };
  then
A2: ex y9 being Element of A st y9 = y & MemberFunc (X, A). y9 > 0;
  then not y in (UAp X)` by Th41;
  hence thesis by A2,XBOOLE_0:def 5;
end;

theorem
  BndAp X = { x where x is Element of A : 0 < MemberFunc (X, A).x &
  MemberFunc (X, A).x < 1 }
proof
  thus BndAp X c= { x where x is Element of A : 0 < MemberFunc (X, A).x &
  MemberFunc (X, A).x < 1 }
  proof
    let y be set;
    assume
A1: y in BndAp X;
    then reconsider y9 = y as Element of A;
    0 < MemberFunc (X, A).y9 & MemberFunc (X, A).y9 < 1 by A1,Th42;
    hence thesis;
  end;
  let y be set;
  assume y in { x where x is Element of A : 0 < MemberFunc (X, A).x &
  MemberFunc (X, A).x < 1 };
  then ex y9 being Element of A st y9 = y & 0 < MemberFunc (X, A).y9 &
  MemberFunc (X, A).y9 < 1;
  hence thesis by Th42;
end;

begin :: Rough Inclusion

reserve A for Tolerance_Space,
  X, Y, Z for Subset of A;

definition
  let A be Tolerance_Space, X, Y be Subset of A;
  pred X _c= Y means
  :Def11:
  LAp X c= LAp Y;
  reflexivity;
  pred X c=^ Y means
  :Def12:
  UAp X c= UAp Y;
  reflexivity;
end;

definition
  let A be Tolerance_Space, X, Y be Subset of A;
  pred X _c=^ Y means
  :Def13:
  X _c= Y & X c=^ Y;
  reflexivity;
end;

theorem Th59:
  X _c= Y & Y _c= Z implies X _c= Z
proof
  assume X _c= Y & Y _c= Z;
  then LAp X c= LAp Y & LAp Y c= LAp Z by Def11;
  then LAp X c= LAp Z by XBOOLE_1:1;
  hence thesis by Def11;
end;

theorem Th60:
  X c=^ Y & Y c=^ Z implies X c=^ Z
proof
  assume X c=^ Y & Y c=^ Z;
  then UAp X c= UAp Y & UAp Y c= UAp Z by Def12;
  then UAp X c= UAp Z by XBOOLE_1:1;
  hence thesis by Def12;
end;

theorem
  X _c=^ Y & Y _c=^ Z implies X _c=^ Z
proof
  assume
A1: X _c=^ Y & Y _c=^ Z;
  then X c=^ Y & Y c=^ Z by Def13;
  then
A2: X c=^ Z by Th60;
  X _c= Y & Y _c= Z by A1,Def13;
  then X _c= Z by Th59;
  hence thesis by A2,Def13;
end;

begin :: Rough Equality of Sets

definition
  let A be Tolerance_Space, X, Y be Subset of A;
  pred X _= Y means
  :Def14:
  LAp X = LAp Y;
  reflexivity;
  symmetry;
  pred X =^ Y means
  :Def15:
  UAp X = UAp Y;
  reflexivity;
  symmetry;
  pred X _=^ Y means
  :Def16:
  LAp X = LAp Y & UAp X = UAp Y;
  reflexivity;
  symmetry;
end;

definition
  let A be Tolerance_Space, X, Y be Subset of A;
  redefine pred X _= Y means
  X _c= Y & Y _c= X;
  compatibility
  proof
    hereby
      assume X _= Y;
      then LAp X = LAp Y by Def14;
      hence X _c= Y & Y _c= X by Def11;
    end;
    assume X _c= Y & Y _c= X;
    then LAp X c= LAp Y & LAp Y c= LAp X by Def11;
    then LAp X = LAp Y by XBOOLE_0:def 10;
    hence thesis by Def14;
  end;
  redefine pred X =^ Y means
  X c=^ Y & Y c=^ X;
  compatibility
  proof
    hereby
      assume X =^ Y;
      then UAp X = UAp Y by Def15;
      hence X c=^ Y & Y c=^ X by Def12;
    end;
    assume X c=^ Y & Y c=^ X;
    then UAp X c= UAp Y & UAp Y c= UAp X by Def12;
    then UAp X = UAp Y by XBOOLE_0:def 10;
    hence thesis by Def15;
  end;
  redefine pred X _=^ Y means
  X _= Y & X =^ Y;
  compatibility
  proof
    hereby
      assume X _=^ Y;
      then LAp X = LAp Y & UAp X = UAp Y by Def16;
      hence X _= Y & X =^ Y by Def14,Def15;
    end;
    assume X _= Y & X =^ Y;
    then LAp X = LAp Y & UAp X = UAp Y by Def14,Def15;
    hence thesis by Def16;
  end;
end;