:: ROUGHS_1 semantic presentation

begin

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

theorem Th1: :: ROUGHS_1:1
for X being set st Total X c= id X holds
X is trivial
proof
let X be set ; ::_thesis: ( Total X c= id X implies X is trivial )
assume A1: Total X c= id X ; ::_thesis: X is trivial
assume  not X is trivial ; ::_thesis: contradiction
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  contradiction by A1, A3, RELAT_1:def_10; ::_thesis: verum
end;

definition
let A be RelStr ;
attrA is diagonal  means :Def1: :: ROUGHS_1:def 1
 the InternalRel of A c= id the carrier of A;
end;

:: deftheorem Def1 defines diagonal ROUGHS_1:def_1_:_
 for A being RelStr holds
( A is diagonal iff the InternalRel of A c= id the carrier of A );

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

theorem :: ROUGHS_1:2
for L being reflexive RelStr holds id the carrier of L c= the InternalRel of L
proof
let L be reflexive RelStr ; ::_thesis: id the carrier of L c= the InternalRel of L
 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 ; ::_thesis: ( [a,b] in id the carrier of L implies [a,b] in the InternalRel of L )
assume  [a,b] in id the carrier of L ; ::_thesis: [a,b] in the InternalRel 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  [a,b] in the InternalRel of L by A1, RELAT_2:def_1; ::_thesis: verum
end;
hence  id the carrier of L c= the InternalRel of L by RELAT_1:def_3; ::_thesis: verum
end;

Lm1:  for A being RelStr st A is reflexive & A is trivial holds
A is discrete
proof
let A be RelStr ; ::_thesis: ( A is reflexive & A is trivial implies A is discrete )
assume A1: ( A is reflexive & A is trivial ) ; ::_thesis: A is discrete
percases ( the carrier of A is empty or ex x being set st the carrier of A = {x} ) by A1, ZFMISC_1:131;
supposeA2: the carrier of A is empty ; ::_thesis: A is discrete
then  the InternalRel of A = {} ;
hence  A is discrete by A2, ORDERS_3:def_1, RELAT_1:55; ::_thesis: verum
end;
suppose ex x being set st the carrier of A = {x} ; ::_thesis: A is discrete
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  A is discrete by A3, ORDERS_3:def_1; ::_thesis: verum
end;
end;
end;

registration
cluster reflexive non discrete  ->  non trivial reflexive for RelStr ;
coherence
 for b1 being reflexive RelStr st not b1 is discrete holds
not b1 is trivial by Lm1;
cluster trivial reflexive  ->  discrete for RelStr ;
coherence
 for b1 being RelStr st b1 is reflexive & b1 is trivial holds
b1 is discrete ;
end;

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

Lm2:  for A being RelStr st A is discrete holds
A is diagonal
proof
let A be RelStr ; ::_thesis: ( A is discrete implies A is diagonal )
assume  A is discrete ; ::_thesis: A is diagonal
then  the InternalRel of A = id the carrier of A by ORDERS_3:def_1;
hence  A is diagonal by Def1; ::_thesis: verum
end;

registration
cluster discrete  ->  diagonal for RelStr ;
coherence
 for b1 being RelStr st b1 is discrete holds
b1 is diagonal by Lm2;
cluster non diagonal  ->  non discrete for RelStr ;
coherence
 for b1 being RelStr st not b1 is diagonal holds
not b1 is discrete ;
end;

registration
cluster non empty non diagonal for RelStr ;
existence
 ex b1 being RelStr st
( not b1 is diagonal & not b1 is empty )
proof
set A = the non trivial set ;
take  RelStr(# the non trivial set ,(Total the non trivial set ) #) ; ::_thesis: ( not RelStr(# the non trivial set ,(Total the non trivial set ) #) is diagonal & not RelStr(# the non trivial set ,(Total the non trivial set ) #) is empty )
thus  ( not RelStr(# the non trivial set ,(Total the non trivial set ) #) is diagonal & not RelStr(# the non trivial set ,(Total the non trivial set ) #) is empty ) ; ::_thesis: verum
end;
end;

theorem Th4: :: ROUGHS_1:4
for A being non empty non diagonal RelStr ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A )
proof
let A be non empty non diagonal RelStr ; ::_thesis: ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A )
now__::_thesis:_(_(_for_x,_y_being_Element_of_A_st_[x,y]_in_the_InternalRel_of_A_holds_
x_=_y_)_implies_ex_x,_y_being_Element_of_A_st_
(_x_<>_y_&_[x,y]_in_the_InternalRel_of_A_)_)
assume A1: for x, y being Element of A st [x,y] in the InternalRel of A holds
x = y ; ::_thesis: ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A )
 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 ; ::_thesis: ( [a,b] in the InternalRel of A implies [a,b] in id the carrier of A )
assume A2: [a,b] in the InternalRel of A ; ::_thesis: [a,b] in id the carrier 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  [a,b] in id the carrier of A by A3, RELAT_1:def_10; ::_thesis: verum
end;
then  the InternalRel of A c= id the carrier of A by RELAT_1:def_3;
hence  ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A ) by Def1; ::_thesis: verum
end;
hence  ex x, y being Element of A st
( x <> y & [x,y] in the InternalRel of A ) ; ::_thesis: verum
end;

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

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

registration
cluster empty Relation-like Function-like  ->  disjoint_valued for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is disjoint_valued
proof
let X be Function; ::_thesis: ( X is empty implies X is disjoint_valued )
assume A1: X is empty ; ::_thesis: X is disjoint_valued
 X is disjoint_valued
proof
let x, y be set ; :: according to PROB_2:def_2 ::_thesis: ( x = y or X . x misses X . y )
assume  x <> y ; ::_thesis: X . x misses X . y
 X . x = {} by A1, FUNCT_1:def_2, RELAT_1:38;
hence  X . x misses X . y by XBOOLE_1:65; ::_thesis: verum
end;
hence  X is disjoint_valued ; ::_thesis: verum
end;
end;

registration
let A be set ;
cluster Relation-like NAT -defined A -valued Function-like finite disjoint_valued FinSequence-like FinSubsequence-like for FinSequence of A;
existence
 ex b1 being FinSequence of A st b1 is disjoint_valued
proof
set X = <*> A;
 <*> A is disjoint_valued ;
hence  ex b1 being FinSequence of A st b1 is disjoint_valued ; ::_thesis: verum
end;
end;

registration
let A be non empty set ;
cluster non empty Relation-like NAT -defined A -valued Function-like finite disjoint_valued FinSequence-like FinSubsequence-like for FinSequence of A;
existence
 ex b1 being FinSequence of A st
( not b1 is empty & b1 is disjoint_valued )
proof
set a = the Element of A;
reconsider X = 1 |-> the Element of A as FinSequence of A ;
A1: X is disjoint_valued
proof
let x, y be set ; :: according to PROB_2:def_2 ::_thesis: ( x = y or X . x misses X . y )
assume A2: x <> y ; ::_thesis: X . x misses X . y
percases ( ( x in dom X & y in dom X ) or not x in dom X or not y in dom X ) ;
supposeA3: ( x in dom X & y in dom X ) ; ::_thesis: X . x misses X . y
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  X . x misses X . y by A2, A4, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
suppose ( not x in dom X or not y in dom X ) ; ::_thesis: X . x misses X . y
then  ( X . x = {} or X . y = {} ) by FUNCT_1:def_2;
hence  X . x misses X . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
 not X is empty by FUNCOP_1:13, RELAT_1:38;
hence  ex b1 being FinSequence of A st
( not b1 is empty & b1 is disjoint_valued ) by A1; ::_thesis: verum
end;
end;

definition
let A be set ;
let X be FinSequence of bool A;
let n be Nat;
:: original: .
redefine funcX . n ->  Subset of A;
coherence
 X . n is Subset of A
proof
percases ( not n in dom X or n in dom X ) ;
suppose not n in dom X ; ::_thesis: X . n is Subset of A
then  X . n = {} by FUNCT_1:def_2;
hence  X . n is Subset of A by XBOOLE_1:2; ::_thesis: verum
end;
suppose n in dom X ; ::_thesis: X . n is Subset of A
hence  X . n is Subset of A by FINSEQ_2:11; ::_thesis: verum
end;
end;
end;
end;

definition
let A be set ;
let X be FinSequence of bool A;
:: original: Union
redefine func Union X ->  Subset of A;
coherence
 Union X is Subset of A
proof
 union (rng X) c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng X) or x in A )
assume  x in union (rng X) ; ::_thesis: x in A
then  ex Y being set st
( x in Y & Y in rng X ) by TARSKI:def_4;
hence  x in A ; ::_thesis: verum
end;
hence  Union X is Subset of A ; ::_thesis: verum
end;
end;

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

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

begin

definition
let P be RelStr ;
attrP is with_equivalence  means :Def2: :: ROUGHS_1:def 2
 the InternalRel of P is Equivalence_Relation of the carrier of P;
attrP is with_tolerance  means :Def3: :: ROUGHS_1:def 3
 the InternalRel of P is Tolerance of the carrier of P;
end;

:: deftheorem Def2 defines with_equivalence ROUGHS_1:def_2_:_
 for P being RelStr holds
( P is with_equivalence iff the InternalRel of P is Equivalence_Relation of the carrier of P );

:: deftheorem Def3 defines with_tolerance ROUGHS_1:def_3_:_
 for P being RelStr holds
( P is with_tolerance iff the InternalRel of P is Tolerance of the carrier of P );

registration
cluster with_equivalence  ->  with_tolerance for RelStr ;
coherence
 for b1 being RelStr st b1 is with_equivalence holds
b1 is with_tolerance
proof
let L be RelStr ; ::_thesis: ( L is with_equivalence implies L is with_tolerance )
assume  L is with_equivalence ; ::_thesis: L is with_tolerance
then  the InternalRel of L is Equivalence_Relation of the carrier of L by Def2;
hence  L is with_tolerance by Def3; ::_thesis: verum
end;
end;

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

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

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

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

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

definition
let A be non empty RelStr ;
let X be Subset of A;
func LAp X ->  Subset of A equals :: ROUGHS_1:def 4
 {  x where x is Element of A : Class ( the InternalRel of A,x) c= X  }  ;
coherence
  {  x where x is Element of A : Class ( the InternalRel of A,x) c= X  }  is Subset of A
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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  x where x is Element of A : Class ( the InternalRel of A,x) c= X  }  or y in the carrier of A )
assume  y in  {  x where x is Element of A : Class ( the InternalRel of A,x) c= X  }  ; ::_thesis: y in the carrier of A
then  ex x being Element of A st
( y = x & Class ( the InternalRel of A,x) c= X ) ;
hence  y in the carrier of A ; ::_thesis: verum
end;
hence   {  x where x is Element of A : Class ( the InternalRel of A,x) c= X  }  is Subset of A ; ::_thesis: verum
end;
func UAp X ->  Subset of A equals :: ROUGHS_1:def 5
 {  x where x is Element of A : Class ( the InternalRel of A,x) meets X  }  ;
coherence
  {  x where x is Element of A : Class ( the InternalRel of A,x) meets X  }  is Subset of A
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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  x where x is Element of A : Class ( the InternalRel of A,x) meets X  }  or y in the carrier of A )
assume  y in  {  x where x is Element of A : Class ( the InternalRel of A,x) meets X  }  ; ::_thesis: y in the carrier of A
then  ex x being Element of A st
( y = x & Class ( the InternalRel of A,x) meets X ) ;
hence  y in the carrier of A ; ::_thesis: verum
end;
hence   {  x where x is Element of A : Class ( the InternalRel of A,x) meets X  }  is Subset of A ; ::_thesis: verum
end;
end;

:: deftheorem  defines LAp ROUGHS_1:def_4_:_
 for A being non empty RelStr
for X being Subset of A holds LAp X =  {  x where x is Element of A : Class ( the InternalRel of A,x) c= X  }  ;

:: deftheorem  defines UAp ROUGHS_1:def_5_:_
 for A being non empty RelStr
for X being Subset of A holds UAp X =  {  x where x is Element of A : Class ( the InternalRel of A,x) meets X  }  ;

definition
let A be non empty RelStr ;
let X be Subset of A;
func BndAp X ->  Subset of A equals :: ROUGHS_1:def 6
(UAp X) \ (LAp X);
coherence
 (UAp X) \ (LAp X) is Subset of A ;
end;

:: deftheorem  defines BndAp ROUGHS_1:def_6_:_
 for A being non empty RelStr
for X being Subset of A holds BndAp X = (UAp X) \ (LAp X);

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

:: deftheorem Def7 defines rough ROUGHS_1:def_7_:_
 for A being non empty RelStr
for X being Subset of A holds
( X is rough iff BndAp X <> {} );

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


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

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

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

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

theorem Th12: :: ROUGHS_1:12
for A being Tolerance_Space
for X being Subset of A holds LAp X c= X
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds LAp X c= X
let X be Subset of A; ::_thesis: LAp X c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LAp X or x in X )
assume  x in LAp X ; ::_thesis: x in 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  x in X by A1; ::_thesis: verum
end;

theorem Th13: :: ROUGHS_1:13
for A being Tolerance_Space
for X being Subset of A holds X c= UAp X
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds X c= UAp X
let X be Subset of A; ::_thesis: X c= UAp X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in UAp X )
assume A1: x in X ; ::_thesis: x in UAp 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  x in UAp X ; ::_thesis: verum
end;

theorem Th14: :: ROUGHS_1:14
for A being Tolerance_Space
for X being Subset of A holds LAp X c= UAp X
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds LAp X c= UAp X
let X be Subset of A; ::_thesis: LAp X c= UAp X
 ( LAp X c= X & X c= UAp X ) by Th12, Th13;
hence  LAp X c= UAp X by XBOOLE_1:1; ::_thesis: verum
end;

theorem Th15: :: ROUGHS_1:15
for A being Tolerance_Space
for X being Subset of A holds
( X is exact iff LAp X = X )
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds
( X is exact iff LAp X = X )
let X be Subset of A; ::_thesis: ( X is exact iff LAp X = X )
A1: LAp X c= UAp X by Th14;
hereby  ::_thesis: ( LAp X = X implies X is exact )
assume  X is exact ; ::_thesis: LAp X = X
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; ::_thesis: verum
end;
assume A3: LAp X = X ; ::_thesis: X is exact
 UAp X c= X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in UAp X or y in X )
assume  y in UAp X ; ::_thesis: y in 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  y in X ; ::_thesis: verum
end;
then  BndAp X = {} by A3, XBOOLE_1:37;
hence  X is exact by Def7; ::_thesis: verum
end;

theorem Th16: :: ROUGHS_1:16
for A being Tolerance_Space
for X being Subset of A holds
( X is exact iff UAp X = X )
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds
( X is exact iff UAp X = X )
let X be Subset of A; ::_thesis: ( X is exact iff UAp X = X )
hereby  ::_thesis: ( UAp X = X implies X is exact )
assume  X is exact ; ::_thesis: UAp X = X
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; ::_thesis: verum
end;
assume A3: UAp X = X ; ::_thesis: X is exact
 X c= LAp X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in LAp X )
assume A4: x in X ; ::_thesis: x in LAp X
 Class ( the InternalRel of A,x) c= X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Class ( the InternalRel of A,x) or y in X )
assume A5: y in Class ( the InternalRel of A,x) ; ::_thesis: y in 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  y in X by A3, A5; ::_thesis: verum
end;
hence  x in LAp X by A4; ::_thesis: verum
end;
then  BndAp X = {} by A3, XBOOLE_1:37;
hence  X is exact by Def7; ::_thesis: verum
end;

theorem :: ROUGHS_1:17
for A being Tolerance_Space
for X being Subset of A holds
( X = LAp X iff X = UAp X )
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds
( X = LAp X iff X = UAp X )
let X be Subset of A; ::_thesis: ( X = LAp X iff X = UAp X )
 ( X = LAp X iff X is exact ) by Th15;
hence  ( X = LAp X iff X = UAp X ) by Th16; ::_thesis: verum
end;

theorem Th18: :: ROUGHS_1:18
for A being Tolerance_Space holds LAp ({} A) = {}
proof
let A be Tolerance_Space; ::_thesis: LAp ({} A) = {}
assume  LAp ({} A) <> {} ; ::_thesis: contradiction
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  contradiction by EQREL_1:20; ::_thesis: verum
end;

theorem Th19: :: ROUGHS_1:19
for A being Tolerance_Space holds UAp ({} A) = {}
proof
let A be Tolerance_Space; ::_thesis: UAp ({} A) = {}
assume  UAp ({} A) <> {} ; ::_thesis: contradiction
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  contradiction by XBOOLE_1:65; ::_thesis: verum
end;

theorem Th20: :: ROUGHS_1:20
for A being Tolerance_Space holds LAp ([#] A) = [#] A
proof
let A be Tolerance_Space; ::_thesis: LAp ([#] A) = [#] A
thus  LAp ([#] A) c= [#] A ; :: according to XBOOLE_0:def_10 ::_thesis: [#] A c= LAp ([#] A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] A or x in LAp ([#] A) )
A1: Class ( the InternalRel of A,x) c= [#] A ;
assume  x in [#] A ; ::_thesis: x in LAp ([#] A)
hence  x in LAp ([#] A) by A1; ::_thesis: verum
end;

theorem :: ROUGHS_1:21
for A being Tolerance_Space holds UAp ([#] A) = [#] A
proof
let A be Tolerance_Space; ::_thesis: UAp ([#] A) = [#] A
 LAp ([#] A) c= UAp ([#] A) by Th14;
then  [#] A c= UAp ([#] A) by Th20;
hence  UAp ([#] A) = [#] A by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: ROUGHS_1:22
for A being Tolerance_Space
for X, Y being Subset of A holds LAp (X /\ Y) = (LAp X) /\ (LAp Y)
proof
let A be Tolerance_Space; ::_thesis: for X, Y being Subset of A holds LAp (X /\ Y) = (LAp X) /\ (LAp Y)
let X, Y be Subset of A; ::_thesis: LAp (X /\ Y) = (LAp X) /\ (LAp Y)
thus  LAp (X /\ Y) c= (LAp X) /\ (LAp Y) :: according to XBOOLE_0:def_10 ::_thesis: (LAp X) /\ (LAp Y) c= LAp (X /\ Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LAp (X /\ Y) or x in (LAp X) /\ (LAp Y) )
assume A1: x in LAp (X /\ Y) ; ::_thesis: x in (LAp X) /\ (LAp 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  x in (LAp X) /\ (LAp Y) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LAp X) /\ (LAp Y) or x in LAp (X /\ Y) )
assume A3: x in (LAp X) /\ (LAp Y) ; ::_thesis: x in LAp (X /\ 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  x in LAp (X /\ Y) by A3; ::_thesis: verum
end;

theorem :: ROUGHS_1:23
for A being Tolerance_Space
for X, Y being Subset of A holds UAp (X \/ Y) = (UAp X) \/ (UAp Y)
proof
let A be Tolerance_Space; ::_thesis: for X, Y being Subset of A holds UAp (X \/ Y) = (UAp X) \/ (UAp Y)
let X, Y be Subset of A; ::_thesis: UAp (X \/ Y) = (UAp X) \/ (UAp Y)
thus  UAp (X \/ Y) c= (UAp X) \/ (UAp Y) :: according to XBOOLE_0:def_10 ::_thesis: (UAp X) \/ (UAp Y) c= UAp (X \/ Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UAp (X \/ Y) or x in (UAp X) \/ (UAp Y) )
assume A1: x in UAp (X \/ Y) ; ::_thesis: x in (UAp X) \/ (UAp 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  x in (UAp X) \/ (UAp Y) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (UAp X) \/ (UAp Y) or x in UAp (X \/ Y) )
assume A2: x in (UAp X) \/ (UAp Y) ; ::_thesis: x in UAp (X \/ 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  x in UAp (X \/ Y) by A2; ::_thesis: verum
end;

theorem Th24: :: ROUGHS_1:24
for A being Tolerance_Space
for X, Y being Subset of A st X c= Y holds
LAp X c= LAp Y
proof
let A be Tolerance_Space; ::_thesis: for X, Y being Subset of A st X c= Y holds
LAp X c= LAp Y
let X, Y be Subset of A; ::_thesis: ( X c= Y implies LAp X c= LAp Y )
assume A1: X c= Y ; ::_thesis: LAp X c= LAp Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LAp X or x in LAp Y )
assume A2: x in LAp X ; ::_thesis: x in LAp Y
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  x in LAp Y by A2; ::_thesis: verum
end;

theorem Th25: :: ROUGHS_1:25
for A being Tolerance_Space
for X, Y being Subset of A st X c= Y holds
UAp X c= UAp Y
proof
let A be Tolerance_Space; ::_thesis: for X, Y being Subset of A st X c= Y holds
UAp X c= UAp Y
let X, Y be Subset of A; ::_thesis: ( X c= Y implies UAp X c= UAp Y )
assume A1: X c= Y ; ::_thesis: UAp X c= UAp Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UAp X or x in UAp Y )
assume A2: x in UAp X ; ::_thesis: x in UAp Y
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  x in UAp Y by A2; ::_thesis: verum
end;

theorem :: ROUGHS_1:26
for A being Tolerance_Space
for X, Y being Subset of A holds (LAp X) \/ (LAp Y) c= LAp (X \/ Y)
proof
let A be Tolerance_Space; ::_thesis: for X, Y being Subset of A holds (LAp X) \/ (LAp Y) c= LAp (X \/ Y)
let X, Y be Subset of A; ::_thesis: (LAp X) \/ (LAp Y) c= LAp (X \/ Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LAp X) \/ (LAp Y) or x in LAp (X \/ Y) )
assume A1: x in (LAp X) \/ (LAp Y) ; ::_thesis: x in LAp (X \/ Y)
percases ( x in LAp X or x in LAp Y ) by A1, XBOOLE_0:def_3;
suppose x in LAp X ; ::_thesis: x in LAp (X \/ Y)
then  Class ( the InternalRel of A,x) c= X \/ Y by Th8, XBOOLE_1:10;
hence  x in LAp (X \/ Y) by A1; ::_thesis: verum
end;
suppose x in LAp Y ; ::_thesis: x in LAp (X \/ Y)
then  Class ( the InternalRel of A,x) c= X \/ Y by Th8, XBOOLE_1:10;
hence  x in LAp (X \/ Y) by A1; ::_thesis: verum
end;
end;
end;

theorem :: ROUGHS_1:27
for A being Tolerance_Space
for X, Y being Subset of A holds UAp (X /\ Y) c= (UAp X) /\ (UAp Y)
proof
let A be Tolerance_Space; ::_thesis: for X, Y being Subset of A holds UAp (X /\ Y) c= (UAp X) /\ (UAp Y)
let X, Y be Subset of A; ::_thesis: UAp (X /\ Y) c= (UAp X) /\ (UAp Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UAp (X /\ Y) or x in (UAp X) /\ (UAp Y) )
assume A1: x in UAp (X /\ Y) ; ::_thesis: x in (UAp X) /\ (UAp 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  x in (UAp X) /\ (UAp Y) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th28: :: ROUGHS_1:28
for A being Tolerance_Space
for X being Subset of A holds LAp (X `) = (UAp X) `
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds LAp (X `) = (UAp X) `
let X be Subset of A; ::_thesis: LAp (X `) = (UAp X) `
 LAp (X `) misses UAp X
proof
assume  LAp (X `) meets UAp X ; ::_thesis: contradiction
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  contradiction by XBOOLE_1:63, XBOOLE_1:79; ::_thesis: verum
end;
hence  LAp (X `) c= (UAp X) ` by SUBSET_1:23; :: according to XBOOLE_0:def_10 ::_thesis: (UAp X) ` c= LAp (X `)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (UAp X) ` or x in LAp (X `) )
assume A2: x in (UAp X) ` ; ::_thesis: x in LAp (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  x in LAp (X `) by A2; ::_thesis: verum
end;

theorem Th29: :: ROUGHS_1:29
for A being Tolerance_Space
for X being Subset of A holds UAp (X `) = (LAp X) `
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds UAp (X `) = (LAp X) `
let X be Subset of A; ::_thesis: UAp (X `) = (LAp X) `
 ((UAp (X `)) `) ` = (LAp ((X `) `)) ` by Th28;
hence  UAp (X `) = (LAp X) ` ; ::_thesis: verum
end;

theorem :: ROUGHS_1:30
for A being Tolerance_Space
for X being Subset of A holds UAp (LAp (UAp X)) = UAp X
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds UAp (LAp (UAp X)) = UAp X
let X be Subset of A; ::_thesis: UAp (LAp (UAp X)) = UAp X
thus  UAp (LAp (UAp X)) c= UAp X :: according to XBOOLE_0:def_10 ::_thesis: UAp X c= UAp (LAp (UAp X))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UAp (LAp (UAp X)) or x in UAp X )
assume  x in UAp (LAp (UAp X)) ; ::_thesis: x in 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  x in UAp X by A3; ::_thesis: verum
end;
 X c= LAp (UAp X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in LAp (UAp X) )
assume A4: x in X ; ::_thesis: x in LAp (UAp X)
 Class ( the InternalRel of A,x) c= UAp X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Class ( the InternalRel of A,x) or y in UAp X )
assume A5: y in Class ( the InternalRel of A,x) ; ::_thesis: y in UAp 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  y in UAp X by A5; ::_thesis: verum
end;
hence  x in LAp (UAp X) by A4; ::_thesis: verum
end;
hence  UAp X c= UAp (LAp (UAp X)) by Th25; ::_thesis: verum
end;

theorem :: ROUGHS_1:31
for A being Tolerance_Space
for X being Subset of A holds LAp (UAp (LAp X)) = LAp X
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds LAp (UAp (LAp X)) = LAp X
let X be Subset of A; ::_thesis: LAp (UAp (LAp X)) = LAp X
 UAp (LAp X) c= X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in UAp (LAp X) or y in X )
assume  y in UAp (LAp X) ; ::_thesis: y in 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  y in X by A3; ::_thesis: verum
end;
hence  LAp (UAp (LAp X)) c= LAp X by Th24; :: according to XBOOLE_0:def_10 ::_thesis: LAp X c= LAp (UAp (LAp X))
thus  LAp X c= LAp (UAp (LAp X)) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LAp X or x in LAp (UAp (LAp X)) )
assume A4: x in LAp X ; ::_thesis: x in LAp (UAp (LAp X))
 Class ( the InternalRel of A,x) c= UAp (LAp X)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Class ( the InternalRel of A,x) or y in UAp (LAp X) )
assume A5: y in Class ( the InternalRel of A,x) ; ::_thesis: y in UAp (LAp 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  y in UAp (LAp X) by A5; ::_thesis: verum
end;
hence  x in LAp (UAp (LAp X)) by A4; ::_thesis: verum
end;
end;

theorem :: ROUGHS_1:32
for A being Tolerance_Space
for X being Subset of A holds BndAp X = BndAp (X `)
proof
let A be Tolerance_Space; ::_thesis: for X being Subset of A holds BndAp X = BndAp (X `)
let X be Subset of A; ::_thesis: BndAp X = BndAp (X `)
thus  BndAp X c= BndAp (X `) :: according to XBOOLE_0:def_10 ::_thesis: BndAp (X `) c= BndAp X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BndAp X or x in BndAp (X `) )
assume A1: x in BndAp X ; ::_thesis: 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  x in BndAp (X `) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  BndAp (X `) c= BndAp X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BndAp (X `) or x in BndAp X )
assume A3: x in BndAp (X `) ; ::_thesis: 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  x in BndAp X by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
end;


theorem :: ROUGHS_1:33
for A being Approximation_Space
for X being Subset of A holds LAp (LAp X) = LAp X
proof
let A be Approximation_Space; ::_thesis: for X being Subset of A holds LAp (LAp X) = LAp X
let X be Subset of A; ::_thesis: LAp (LAp X) = LAp X
thus  LAp (LAp X) c= LAp X by Th12; :: according to XBOOLE_0:def_10 ::_thesis: LAp X c= LAp (LAp X)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LAp X or x in LAp (LAp X) )
assume A1: x in LAp X ; ::_thesis: x in LAp (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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in Class ( the InternalRel of A,x) or y in LAp X )
assume A3: y in Class ( the InternalRel of A,x) ; ::_thesis: y in LAp X
then  Class ( the InternalRel of A,x) = Class ( the InternalRel of A,y) by A1, EQREL_1:23;
hence  y in LAp X by A2, A3; ::_thesis: verum
end;
hence  x in LAp (LAp X) by A1; ::_thesis: verum
end;

theorem Th34: :: ROUGHS_1:34
for A being Approximation_Space
for X being Subset of A holds LAp (LAp X) = UAp (LAp X)
proof
let A be Approximation_Space; ::_thesis: for X being Subset of A holds LAp (LAp X) = UAp (LAp X)
let X be Subset of A; ::_thesis: LAp (LAp X) = UAp (LAp X)
thus  LAp (LAp X) c= UAp (LAp X) by Th14; :: according to XBOOLE_0:def_10 ::_thesis: UAp (LAp X) c= LAp (LAp X)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UAp (LAp X) or x in LAp (LAp X) )
assume A1: x in UAp (LAp X) ; ::_thesis: x in LAp (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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in Class ( the InternalRel of A,x) or y in LAp X )
assume A5: y in Class ( the InternalRel of A,x) ; ::_thesis: y in LAp X
then  Class ( the InternalRel of A,x) = Class ( the InternalRel of A,y) by A1, EQREL_1:23;
hence  y in LAp X by A4, A5; ::_thesis: verum
end;
hence  x in LAp (LAp X) by A1; ::_thesis: verum
end;

theorem :: ROUGHS_1:35
for A being Approximation_Space
for X being Subset of A holds UAp (UAp X) = UAp X
proof
let A be Approximation_Space; ::_thesis: for X being Subset of A holds UAp (UAp X) = UAp X
let X be Subset of A; ::_thesis: UAp (UAp X) = UAp X
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: UAp X c= UAp (UAp X)
let x be set ; ::_thesis: ( x in UAp (UAp X) implies x in UAp X )
assume A1: x in UAp (UAp X) ; ::_thesis: x in 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; ::_thesis: verum
end;
thus  UAp X c= UAp (UAp X) by Th13; ::_thesis: verum
end;

theorem Th36: :: ROUGHS_1:36
for A being Approximation_Space
for X being Subset of A holds UAp (UAp X) = LAp (UAp X)
proof
let A be Approximation_Space; ::_thesis: for X being Subset of A holds UAp (UAp X) = LAp (UAp X)
let X be Subset of A; ::_thesis: UAp (UAp X) = LAp (UAp X)
thus  UAp (UAp X) c= LAp (UAp X) :: according to XBOOLE_0:def_10 ::_thesis: LAp (UAp X) c= UAp (UAp X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UAp (UAp X) or x in LAp (UAp X) )
assume A1: x in UAp (UAp X) ; ::_thesis: x in LAp (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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in Class ( the InternalRel of A,x) or y in UAp X )
assume A6: y in Class ( the InternalRel of A,x) ; ::_thesis: y in UAp X
then  Class ( the InternalRel of A,x) = Class ( the InternalRel of A,y) by A1, EQREL_1:23;
hence  y in UAp X by A5, A4, A6; ::_thesis: verum
end;
hence  x in LAp (UAp X) by A1; ::_thesis: verum
end;
thus  LAp (UAp X) c= UAp (UAp X) by Th14; ::_thesis: verum
end;

registration
let A be Tolerance_Space;
cluster exact for Element of bool the carrier of A;
existence
 ex b1 being Subset of A st b1 is exact
proof
take  {} A ; ::_thesis: {} A is exact
 LAp ({} A) = {} by Th18;
hence  {} A is exact by Th15; ::_thesis: verum
end;
end;

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

theorem Th37: :: ROUGHS_1:37
for A being Approximation_Space
for X being Subset of A
for 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; ::_thesis: for X being Subset of A
for x, y being set st x in UAp X & [x,y] in the InternalRel of A holds
y in UAp X
let X be Subset of A; ::_thesis: for x, y being set st x in UAp X & [x,y] in the InternalRel of A holds
y in UAp X
let x, y be set ; ::_thesis: ( x in UAp X & [x,y] in the InternalRel of A implies y in UAp X )
assume that
A1: x in UAp X and
A2: [x,y] in the InternalRel of A ; ::_thesis: y in UAp X
 [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  y in UAp X by A3; ::_thesis: verum
end;

registration
let A be non diagonal Approximation_Space;
cluster rough for Element of bool the carrier of A;
existence
 ex b1 being Subset of A st b1 is rough
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  not {x} is exact by Th16;
hence  ex b1 being Subset of A st b1 is rough ; ::_thesis: verum
end;
end;

definition
let A be Approximation_Space;
let X be Subset of A;
mode RoughSet of X ->  set  means :: ROUGHS_1:def 8
it = [(LAp X),(UAp X)];
existence
 ex b1 being set st b1 = [(LAp X),(UAp X)] ;
end;

:: deftheorem  defines RoughSet ROUGHS_1:def_8_:_
 for A being Approximation_Space
for X being Subset of A
for b3 being set holds
( b3 is RoughSet of X iff b3 = [(LAp X),(UAp X)] );

begin

registration
let A be finite Tolerance_Space;
let x be Element of A;
cluster card (Class ( the InternalRel of A,x)) ->  non empty ;
coherence
 not card (Class ( the InternalRel of A,x)) is empty
proof
 x in Class ( the InternalRel of A,x) by EQREL_1:20;
hence  not card (Class ( the InternalRel of A,x)) is empty ; ::_thesis: verum
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: :: ROUGHS_1:def 9
 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
 ex b1 being Function of the carrier of A,REAL st
for x being Element of A holds b1 . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x)))
proof
deffunc H1( set ) ->  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
H1(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 = H1(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 = H1(x) ;
take  f ; ::_thesis: for x being Element of A holds f . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x)))
let x be Element of A; ::_thesis: f . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x)))
thus  f . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the carrier of A,REAL st ( for x being Element of A holds b1 . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) ) & ( for x being Element of A holds b2 . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) ) holds
b1 = b2
proof
deffunc H1( Element of A) ->  set = (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 = H1(x) ) & ( for x being Element of A holds A2 . x = H1(x) ) holds
A1 = A2 from BINOP_2:sch_1();
let A1, A2 be Function of the carrier of A,REAL; ::_thesis: ( ( for x being Element of A holds A1 . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) ) & ( for x being Element of A holds A2 . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) ) implies A1 = A2 )
assume  ( ( for x being Element of A holds A1 . x = H1(x) ) & ( for x being Element of A holds A2 . x = H1(x) ) ) ; ::_thesis: A1 = A2
hence  A1 = A2 by A3; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines MemberFunc ROUGHS_1:def_9_:_
 for A being finite Tolerance_Space
for X being Subset of A
for b3 being Function of the carrier of A,REAL holds
( b3 = MemberFunc (X,A) iff for x being Element of A holds b3 . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) );


theorem Th38: :: ROUGHS_1:38
for A being finite Tolerance_Space
for X being Subset of A
for x being Element of A holds
( 0 <= (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x <= 1 )
proof
let A be finite Tolerance_Space; ::_thesis: for X being Subset of A
for x being Element of A holds
( 0 <= (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x <= 1 )
let X be Subset of A; ::_thesis: for x being Element of A holds
( 0 <= (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x <= 1 )
let x be Element of A; ::_thesis: ( 0 <= (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x <= 1 )
 (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) >= 0 ;
hence  0 <= (MemberFunc (X,A)) . x by Def9; ::_thesis: (MemberFunc (X,A)) . x <= 1
 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  (MemberFunc (X,A)) . x <= 1 by Def9; ::_thesis: verum
end;

theorem :: ROUGHS_1:39
for A being finite Tolerance_Space
for X being Subset of A
for x being Element of A holds (MemberFunc (X,A)) . x in [.0,1.]
proof
let A be finite Tolerance_Space; ::_thesis: for X being Subset of A
for x being Element of A holds (MemberFunc (X,A)) . x in [.0,1.]
let X be Subset of A; ::_thesis: for x being Element of A holds (MemberFunc (X,A)) . x in [.0,1.]
let x be Element of A; ::_thesis: (MemberFunc (X,A)) . x in [.0,1.]
 ( 0 <= (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x <= 1 ) by Th38;
hence  (MemberFunc (X,A)) . x in [.0,1.] by XXREAL_1:1; ::_thesis: verum
end;


theorem Th40: :: ROUGHS_1:40
for A being finite Approximation_Space
for X being Subset of A
for x being Element of A holds
( (MemberFunc (X,A)) . x = 1 iff x in LAp X )
proof
let A be finite Approximation_Space; ::_thesis: for X being Subset of A
for x being Element of A holds
( (MemberFunc (X,A)) . x = 1 iff x in LAp X )
let X be Subset of A; ::_thesis: for x being Element of A holds
( (MemberFunc (X,A)) . x = 1 iff x in LAp X )
let x be Element of A; ::_thesis: ( (MemberFunc (X,A)) . x = 1 iff x in LAp X )
hereby  ::_thesis: ( x in LAp X implies (MemberFunc (X,A)) . x = 1 )
assume A1: (MemberFunc (X,A)) . x = 1 ; ::_thesis: x in LAp X
 (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 ; ::_thesis: verum
end;
assume  x in LAp X ; ::_thesis: (MemberFunc (X,A)) . x = 1
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  (MemberFunc (X,A)) . x = 1 by A2, XCMPLX_1:60; ::_thesis: verum
end;

theorem Th41: :: ROUGHS_1:41
for A being finite Approximation_Space
for X being Subset of A
for x being Element of A holds
( (MemberFunc (X,A)) . x = 0 iff x in (UAp X) ` )
proof
let A be finite Approximation_Space; ::_thesis: for X being Subset of A
for x being Element of A holds
( (MemberFunc (X,A)) . x = 0 iff x in (UAp X) ` )
let X be Subset of A; ::_thesis: for x being Element of A holds
( (MemberFunc (X,A)) . x = 0 iff x in (UAp X) ` )
let x be Element of A; ::_thesis: ( (MemberFunc (X,A)) . x = 0 iff x in (UAp X) ` )
hereby  ::_thesis: ( x in (UAp X) ` implies (MemberFunc (X,A)) . x = 0 )
assume A1: (MemberFunc (X,A)) . x = 0 ; ::_thesis: x in (UAp X) `
 (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; ::_thesis: verum
end;
assume  x in (UAp X) ` ; ::_thesis: (MemberFunc (X,A)) . x = 0
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  (MemberFunc (X,A)) . x = 0 by A2; ::_thesis: verum
end;

theorem Th42: :: ROUGHS_1:42
for A being finite Approximation_Space
for X being Subset of A
for x being Element of A holds
( ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) iff x in BndAp X )
proof
let A be finite Approximation_Space; ::_thesis: for X being Subset of A
for x being Element of A holds
( ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) iff x in BndAp X )
let X be Subset of A; ::_thesis: for x being Element of A holds
( ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) iff x in BndAp X )
let x be Element of A; ::_thesis: ( ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) iff x in BndAp X )
hereby  ::_thesis: ( x in BndAp X implies ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) )
assume that
A1: 0 < (MemberFunc (X,A)) . x and
A2: (MemberFunc (X,A)) . x < 1 ; ::_thesis: x in BndAp X
 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; ::_thesis: verum
end;
assume A4: x in BndAp X ; ::_thesis: ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )
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  ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) by A6, A5, Th38, XXREAL_0:1; ::_thesis: verum
end;

theorem Th43: :: ROUGHS_1:43
for A being discrete Approximation_Space
for X being Subset of A holds X is exact
proof
let A be discrete Approximation_Space; ::_thesis: for X being Subset of A holds X is exact
let X be Subset of A; ::_thesis: X is exact
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; :: according to XBOOLE_0:def_10 ::_thesis: UAp X c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UAp X or x in X )
assume A2: x in UAp X ; ::_thesis: x in 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  x in X by A3, TARSKI:def_1; ::_thesis: verum
end;
hence  X is exact ; ::_thesis: verum
end;

registration
let A be discrete Approximation_Space;
cluster  ->  exact for Element of bool the carrier of A;
coherence
 for b1 being Subset of A holds b1 is exact by Th43;
end;

theorem :: ROUGHS_1:44
for A being finite discrete Approximation_Space
for X being Subset of A holds MemberFunc (X,A) = chi (X, the carrier of A)
proof
let A be finite discrete Approximation_Space; ::_thesis: for X being Subset of A holds MemberFunc (X,A) = chi (X, the carrier of A)
let X be Subset of A; ::_thesis: MemberFunc (X,A) = chi (X, the carrier 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} c= REAL ;
then reconsider G = chi (X, the carrier of A) 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 ; ::_thesis: ( x in the carrier of A implies F . x = G . x )
assume A1: x in the carrier of A ; ::_thesis: F . x = G . x
percases ( x in X or not x in X ) ;
supposeA2: x in X ; ::_thesis: F . x = G . x
then  x in LAp X by Th15;
then  F . x = 1 by Th40;
hence  F . x = G . x by A2, FUNCT_3:def_3; ::_thesis: verum
end;
supposeA3: not x in X ; ::_thesis: F . x = G . 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  F . x = G . x by A1, A3, FUNCT_3:def_3; ::_thesis: verum
end;
end;
end;
hence  MemberFunc (X,A) = chi (X, the carrier of A) by FUNCT_2:12; ::_thesis: verum
end;

theorem :: ROUGHS_1:45
for A being finite Approximation_Space
for X being Subset of A
for 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; ::_thesis: for X being Subset of A
for x, y being set st [x,y] in the InternalRel of A holds
(MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y
let X be Subset of A; ::_thesis: for x, y being set st [x,y] in the InternalRel of A holds
(MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y
let x, y be set ; ::_thesis: ( [x,y] in the InternalRel of A implies (MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y )
assume A1: [x,y] in the InternalRel of A ; ::_thesis: (MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y
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  (MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y by A2, A3, Def9; ::_thesis: verum
end;

theorem :: ROUGHS_1:46
for A being finite Approximation_Space
for X being Subset of A
for x being Element of A holds (MemberFunc ((X `),A)) . x = 1 - ((MemberFunc (X,A)) . x)
proof
let A be finite Approximation_Space; ::_thesis: for X being Subset of A
for x being Element of A holds (MemberFunc ((X `),A)) . x = 1 - ((MemberFunc (X,A)) . x)
let X be Subset of A; ::_thesis: for x being Element of A holds (MemberFunc ((X `),A)) . x = 1 - ((MemberFunc (X,A)) . x)
let x be Element of A; ::_thesis: (MemberFunc ((X `),A)) . x = 1 - ((MemberFunc (X,A)) . x)
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  (MemberFunc ((X `),A)) . x = 1 - ((MemberFunc (X,A)) . x) ; ::_thesis: verum
end;

theorem Th47: :: ROUGHS_1:47
for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A st X c= Y holds
(MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x
proof
let A be finite Approximation_Space; ::_thesis: for X, Y being Subset of A
for x being Element of A st X c= Y holds
(MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x
let X, Y be Subset of A; ::_thesis: for x being Element of A st X c= Y holds
(MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x
let x be Element of A; ::_thesis: ( X c= Y implies (MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x )
set CI = Class ( the InternalRel of A,x);
assume  X c= Y ; ::_thesis: (MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x
then  card (Y /\ (Class ( the InternalRel of A,x))) >= card (X /\ (Class ( the InternalRel of A,x))) by NAT_1:43, XBOOLE_1:26;
then A1: (card (Y /\ (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 XREAL_1:72;
 (MemberFunc (X,A)) . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) by Def9;
hence  (MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x by A1, Def9; ::_thesis: verum
end;

theorem :: ROUGHS_1:48
for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A holds (MemberFunc ((X \/ Y),A)) . x >= (MemberFunc (X,A)) . x by Th47, XBOOLE_1:7;

theorem :: ROUGHS_1:49
for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A holds (MemberFunc ((X /\ Y),A)) . x <= (MemberFunc (X,A)) . x by Th47, XBOOLE_1:17;

theorem :: ROUGHS_1:50
for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A holds (MemberFunc ((X \/ Y),A)) . x >= max (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x))
proof
let A be finite Approximation_Space; ::_thesis: for X, Y being Subset of A
for x being Element of A holds (MemberFunc ((X \/ Y),A)) . x >= max (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x))
let X, Y be Subset of A; ::_thesis: for x being Element of A holds (MemberFunc ((X \/ Y),A)) . x >= max (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x))
let x be Element of A; ::_thesis: (MemberFunc ((X \/ Y),A)) . x >= max (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x))
 ( (MemberFunc ((X \/ Y),A)) . x >= (MemberFunc (X,A)) . x & (MemberFunc ((X \/ Y),A)) . x >= (MemberFunc (Y,A)) . x ) by Th47, XBOOLE_1:7;
hence  (MemberFunc ((X \/ Y),A)) . x >= max (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x)) by XXREAL_0:28; ::_thesis: verum
end;

theorem Th51: :: ROUGHS_1:51
for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A st X misses Y holds
(MemberFunc ((X \/ Y),A)) . x = ((MemberFunc (X,A)) . x) + ((MemberFunc (Y,A)) . x)
proof
let A be finite Approximation_Space; ::_thesis: for X, Y being Subset of A
for x being Element of A st X misses Y holds
(MemberFunc ((X \/ Y),A)) . x = ((MemberFunc (X,A)) . x) + ((MemberFunc (Y,A)) . x)
let X, Y be Subset of A; ::_thesis: for x being Element of A st X misses Y holds
(MemberFunc ((X \/ Y),A)) . x = ((MemberFunc (X,A)) . x) + ((MemberFunc (Y,A)) . x)
let x be Element of A; ::_thesis: ( X misses Y implies (MemberFunc ((X \/ Y),A)) . x = ((MemberFunc (X,A)) . x) + ((MemberFunc (Y,A)) . x) )
assume A1: X misses Y ; ::_thesis: (MemberFunc ((X \/ Y),A)) . x = ((MemberFunc (X,A)) . x) + ((MemberFunc (Y,A)) . x)
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  (MemberFunc ((X \/ Y),A)) . x = ((MemberFunc (X,A)) . x) + ((MemberFunc (Y,A)) . x) ; ::_thesis: verum
end;

theorem :: ROUGHS_1:52
for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A holds (MemberFunc ((X /\ Y),A)) . x <= min (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x))
proof
let A be finite Approximation_Space; ::_thesis: for X, Y being Subset of A
for x being Element of A holds (MemberFunc ((X /\ Y),A)) . x <= min (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x))
let X, Y be Subset of A; ::_thesis: for x being Element of A holds (MemberFunc ((X /\ Y),A)) . x <= min (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x))
let x be Element of A; ::_thesis: (MemberFunc ((X /\ Y),A)) . x <= min (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x))
 ( (MemberFunc ((X /\ Y),A)) . x <= (MemberFunc (X,A)) . x & (MemberFunc ((X /\ Y),A)) . x <= (MemberFunc (Y,A)) . x ) by Th47, XBOOLE_1:17;
hence  (MemberFunc ((X /\ Y),A)) . x <= min (((MemberFunc (X,A)) . x),((MemberFunc (Y,A)) . x)) by XXREAL_0:20; ::_thesis: verum
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: :: ROUGHS_1:def 10
( dom it = dom X & ( for n being Nat st n in dom X holds
it . n = (MemberFunc ((X . n),A)) . x ) );
existence
 ex b1 being FinSequence of REAL st
( dom b1 = dom X & ( for n being Nat st n in dom X holds
b1 . n = (MemberFunc ((X . n),A)) . x ) )
proof
deffunc H1( Nat) ->  Element of REAL = (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 = H1(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 = H1(j) ;
take  z ; ::_thesis: ( dom z = dom X & ( for n being Nat st n in dom X holds
z . n = (MemberFunc ((X . n),A)) . x ) )
thus  dom z = Seg (len z) by FINSEQ_1:def_3
.= dom X by A1, FINSEQ_1:def_3 ; ::_thesis: for n being Nat st n in dom X holds
z . n = (MemberFunc ((X . n),A)) . x
let n be Nat; ::_thesis: ( n in dom X implies z . n = (MemberFunc ((X . n),A)) . x )
assume  n in dom X ; ::_thesis: z . n = (MemberFunc ((X . n),A)) . 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  z . n = (MemberFunc ((X . n),A)) . x by A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of REAL st dom b1 = dom X & ( for n being Nat st n in dom X holds
b1 . n = (MemberFunc ((X . n),A)) . x ) & dom b2 = dom X & ( for n being Nat st n in dom X holds
b2 . n = (MemberFunc ((X . n),A)) . x ) holds
b1 = b2
proof
let A1, A2 be FinSequence of REAL ; ::_thesis: ( dom A1 = dom X & ( for n being Nat st n in dom X holds
A1 . n = (MemberFunc ((X . n),A)) . x ) & dom A2 = dom X & ( for n being Nat st n in dom X holds
A2 . n = (MemberFunc ((X . n),A)) . x ) implies A1 = A2 )
assume 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 ; ::_thesis: A1 = A2
 for n being Nat st n in dom A1 holds
A1 . n = A2 . n
proof
let n be Nat; ::_thesis: ( n in dom A1 implies A1 . n = A2 . n )
assume A8: n in dom A1 ; ::_thesis: A1 . n = A2 . n
reconsider n = 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  A1 . n = A2 . n ; ::_thesis: verum
end;
hence  A1 = A2 by A4, A6, FINSEQ_1:13; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines FinSeqM ROUGHS_1:def_10_:_
 for A being finite Tolerance_Space
for X being FinSequence of bool the carrier of A
for x being Element of A
for b4 being FinSequence of REAL holds
( b4 = FinSeqM (x,X) iff ( dom b4 = dom X & ( for n being Nat st n in dom X holds
b4 . n = (MemberFunc ((X . n),A)) . x ) ) );

theorem Th53: :: ROUGHS_1:53
for A being finite Approximation_Space
for X being FinSequence of bool the carrier of A
for x being Element of A
for y being Subset of A holds FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>
proof
let A be finite Approximation_Space; ::_thesis: for X being FinSequence of bool the carrier of A
for x being Element of A
for y being Subset of A holds FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>
let X be FinSequence of bool the carrier of A; ::_thesis: for x being Element of A
for y being Subset of A holds FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>
let x be Element of A; ::_thesis: for y being Subset of A holds FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>
let y be Subset of A; ::_thesis: FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>
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 (FinSeqM (x,(X ^ <*y*>))) = 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 (FinSeqM (x,(X ^ <*y*>))) holds
(FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k
proof
let k be Nat; ::_thesis: ( k in dom (FinSeqM (x,(X ^ <*y*>))) implies (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k )
assume A4: k in dom (FinSeqM (x,(X ^ <*y*>))) ; ::_thesis: (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k
then reconsider k = k as Element of NAT ;
A5: 1 <= k by A4, FINSEQ_3:25;
 k in dom (X ^ <*y*>) by A4, Def10;
then A6: (FinSeqM (x,(X ^ <*y*>))) . k = (MemberFunc (((X ^ <*y*>) . k),A)) . x by Def10;
A7: k <= (len X) + 1 by A2, A4, FINSEQ_1:1;
percases ( k <= len X or k = (len X) + 1 ) by A7, NAT_1:8;
supposeA8: k <= len X ; ::_thesis: (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k
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 ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k = (FinSeqM (x,X)) . k by FINSEQ_1:def_7
.= (MemberFunc ((X . k),A)) . x by A9, Def10 ;
hence  (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k by A6, A9, FINSEQ_1:def_7; ::_thesis: verum
end;
supposeA10: k = (len X) + 1 ; ::_thesis: (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k
then  ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k = (MemberFunc (y,A)) . x by A1, FINSEQ_1:42;
hence  (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k by A6, A10, FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
dom ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) = 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  FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*> by A2, A3, FINSEQ_1:13; ::_thesis: verum
end;

theorem Th54: :: ROUGHS_1:54
for A being finite Approximation_Space
for x being Element of A holds (MemberFunc (({} A),A)) . x = 0
proof
let A be finite Approximation_Space; ::_thesis: for x being Element of A holds (MemberFunc (({} A),A)) . x = 0
let x be Element of A; ::_thesis: (MemberFunc (({} A),A)) . x = 0
 UAp ({} A) = {} by Th19;
then  (UAp ({} A)) ` = [#] A ;
hence  (MemberFunc (({} A),A)) . x = 0 by Th41; ::_thesis: verum
end;

theorem :: ROUGHS_1:55
for A being finite Approximation_Space
for x being Element of A
for X being disjoint_valued FinSequence of bool the carrier of A holds (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X))
proof
let A be finite Approximation_Space; ::_thesis: for x being Element of A
for X being disjoint_valued FinSequence of bool the carrier of A holds (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X))
let x be Element of A; ::_thesis: for X being disjoint_valued FinSequence of bool the carrier of A holds (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X))
let X be disjoint_valued FinSequence of bool the carrier of A; ::_thesis: (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X))
defpred S1[ 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 S1[p] holds
S1[p ^ <*y*>]
proof
let p be FinSequence of bool the carrier of A; ::_thesis: for y being Subset of A st S1[p] holds
S1[p ^ <*y*>]
let y be Subset of A; ::_thesis: ( S1[p] implies S1[p ^ <*y*>] )
assume A2: S1[p] ; ::_thesis: S1[p ^ <*y*>]
 S1[p ^ <*y*>]
proof
assume A3: p ^ <*y*> is disjoint_valued ; ::_thesis: (MemberFunc ((Union (p ^ <*y*>)),A)) . x = Sum (FinSeqM (x,(p ^ <*y*>)))
A4: Union p misses y
proof
assume  Union p meets y ; ::_thesis: contradiction
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 = 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  contradiction by A3, A12, A11, PROB_2:def_2; ::_thesis: verum
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  (MemberFunc ((Union (p ^ <*y*>)),A)) . x = Sum (FinSeqM (x,(p ^ <*y*>))) ; ::_thesis: verum
end;
hence  S1[p ^ <*y*>] ; ::_thesis: verum
end;
A13: S1[ <*> (bool the carrier of A)]
proof
set F = FinSeqM (x,(<*> (bool the carrier of A)));
assume  <*> (bool the carrier of A) is disjoint_valued ; ::_thesis: (MemberFunc ((Union (<*> (bool the carrier of A))),A)) . x = Sum (FinSeqM (x,(<*> (bool the carrier of A))))
 dom (FinSeqM (x,(<*> (bool the carrier of A)))) = dom (<*> (bool the carrier of A)) by Def10;
then A14: Sum (FinSeqM (x,(<*> (bool the carrier of A)))) = 0 by RELAT_1:41, RVSUM_1:72;
 Union (<*> (bool the carrier of A)) = {} A by ZFMISC_1:2;
hence  (MemberFunc ((Union (<*> (bool the carrier of A))),A)) . x = Sum (FinSeqM (x,(<*> (bool the carrier of A)))) by A14, Th54; ::_thesis: verum
end;
 for p being FinSequence of bool the carrier of A holds S1[p] from FINSEQ_2:sch_2(A13, A1);
hence  (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X)) ; ::_thesis: verum
end;

theorem :: ROUGHS_1:56
for A being finite Approximation_Space
for X being Subset of A holds LAp X =  {  x where x is Element of A : (MemberFunc (X,A)) . x = 1  }
proof
let A be finite Approximation_Space; ::_thesis: for X being Subset of A holds LAp X =  {  x where x is Element of A : (MemberFunc (X,A)) . x = 1  }
let X be Subset of A; ::_thesis: LAp X =  {  x where x is Element of A : (MemberFunc (X,A)) . x = 1  }
thus  LAp X c=  {  x where x is Element of A : (MemberFunc (X,A)) . x = 1  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x where x is Element of A : (MemberFunc (X,A)) . x = 1  }  c= LAp X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in LAp X or y in  {  x where x is Element of A : (MemberFunc (X,A)) . x = 1  }  )
assume A1: y in LAp X ; ::_thesis: y in  {  x where x is Element of A : (MemberFunc (X,A)) . x = 1  }
then reconsider y9 = y as Element of A ;
 (MemberFunc (X,A)) . y9 = 1 by A1, Th40;
hence  y in  {  x where x is Element of A : (MemberFunc (X,A)) . x = 1  }  ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  x where x is Element of A : (MemberFunc (X,A)) . x = 1  }  or y in LAp X )
assume  y in  {  x where x is Element of A : (MemberFunc (X,A)) . x = 1  }  ; ::_thesis: y in LAp X
then  ex y9 being Element of A st
( y9 = y & (MemberFunc (X,A)) . y9 = 1 ) ;
hence  y in LAp X by Th40; ::_thesis: verum
end;

theorem :: ROUGHS_1:57
for A being finite Approximation_Space
for X being Subset of A holds UAp X =  {  x where x is Element of A : (MemberFunc (X,A)) . x > 0  }
proof
let A be finite Approximation_Space; ::_thesis: for X being Subset of A holds UAp X =  {  x where x is Element of A : (MemberFunc (X,A)) . x > 0  }
let X be Subset of A; ::_thesis: UAp X =  {  x where x is Element of A : (MemberFunc (X,A)) . x > 0  }
thus  UAp X c=  {  x where x is Element of A : (MemberFunc (X,A)) . x > 0  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x where x is Element of A : (MemberFunc (X,A)) . x > 0  }  c= UAp X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in UAp X or y in  {  x where x is Element of A : (MemberFunc (X,A)) . x > 0  }  )
assume A1: y in UAp X ; ::_thesis: y in  {  x where x is Element of A : (MemberFunc (X,A)) . x > 0  }
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  y in  {  x where x is Element of A : (MemberFunc (X,A)) . x > 0  }  ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  x where x is Element of A : (MemberFunc (X,A)) . x > 0  }  or y in UAp X )
assume  y in  {  x where x is Element of A : (MemberFunc (X,A)) . x > 0  }  ; ::_thesis: y in UAp X
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  y in UAp X by A2, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: ROUGHS_1:58
for A being finite Approximation_Space
for X being Subset of A holds BndAp X =  {  x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )  }
proof
let A be finite Approximation_Space; ::_thesis: for X being Subset of A holds BndAp X =  {  x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )  }
let X be Subset of A; ::_thesis: BndAp X =  {  x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )  }
thus  BndAp X c=  {  x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )  }  c= BndAp X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in BndAp X or y in  {  x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )  }  )
assume A1: y in BndAp X ; ::_thesis: y in  {  x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )  }
then reconsider y9 = y as Element of A ;
 ( 0 < (MemberFunc (X,A)) . y9 & (MemberFunc (X,A)) . y9 < 1 ) by A1, Th42;
hence  y in  {  x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )  }  ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )  }  or y in BndAp X )
assume  y in  {  x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 )  }  ; ::_thesis: y in BndAp X
then  ex y9 being Element of A st
( y9 = y & 0 < (MemberFunc (X,A)) . y9 & (MemberFunc (X,A)) . y9 < 1 ) ;
hence  y in BndAp X by Th42; ::_thesis: verum
end;

begin


definition
let A be Tolerance_Space;
let X, Y be Subset of A;
predX _c= Y means :Def11: :: ROUGHS_1:def 11
 LAp X c= LAp Y;
reflexivity
 for X being Subset of A holds LAp X c= LAp X ;
predX c=^ Y means :Def12: :: ROUGHS_1:def 12
 UAp X c= UAp Y;
reflexivity
 for X being Subset of A holds UAp X c= UAp X ;
end;

:: deftheorem Def11 defines _c= ROUGHS_1:def_11_:_
 for A being Tolerance_Space
for X, Y being Subset of A holds
( X _c= Y iff LAp X c= LAp Y );

:: deftheorem Def12 defines c=^ ROUGHS_1:def_12_:_
 for A being Tolerance_Space
for X, Y being Subset of A holds
( X c=^ Y iff UAp X c= UAp Y );

definition
let A be Tolerance_Space;
let X, Y be Subset of A;
predX _c=^ Y means :Def13: :: ROUGHS_1:def 13
( X _c= Y & X c=^ Y );
reflexivity
 for X being Subset of A holds
( X _c= X & X c=^ X ) ;
end;

:: deftheorem Def13 defines _c=^ ROUGHS_1:def_13_:_
 for A being Tolerance_Space
for X, Y being Subset of A holds
( X _c=^ Y iff ( X _c= Y & X c=^ Y ) );

theorem Th59: :: ROUGHS_1:59
for A being Tolerance_Space
for X, Y, Z being Subset of A st X _c= Y & Y _c= Z holds
X _c= Z
proof
let A be Tolerance_Space; ::_thesis: for X, Y, Z being Subset of A st X _c= Y & Y _c= Z holds
X _c= Z
let X, Y, Z be Subset of A; ::_thesis: ( X _c= Y & Y _c= Z implies X _c= Z )
assume  ( X _c= Y & Y _c= Z ) ; ::_thesis: X _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  X _c= Z by Def11; ::_thesis: verum
end;

theorem Th60: :: ROUGHS_1:60
for A being Tolerance_Space
for X, Y, Z being Subset of A st X c=^ Y & Y c=^ Z holds
X c=^ Z
proof
let A be Tolerance_Space; ::_thesis: for X, Y, Z being Subset of A st X c=^ Y & Y c=^ Z holds
X c=^ Z
let X, Y, Z be Subset of A; ::_thesis: ( X c=^ Y & Y c=^ Z implies X c=^ Z )
assume  ( X c=^ Y & Y c=^ Z ) ; ::_thesis: X 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  X c=^ Z by Def12; ::_thesis: verum
end;

theorem :: ROUGHS_1:61
for A being Tolerance_Space
for X, Y, Z being Subset of A st X _c=^ Y & Y _c=^ Z holds
X _c=^ Z
proof
let A be Tolerance_Space; ::_thesis: for X, Y, Z being Subset of A st X _c=^ Y & Y _c=^ Z holds
X _c=^ Z
let X, Y, Z be Subset of A; ::_thesis: ( X _c=^ Y & Y _c=^ Z implies X _c=^ Z )
assume A1: ( X _c=^ Y & Y _c=^ Z ) ; ::_thesis: X _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  X _c=^ Z by A2, Def13; ::_thesis: verum
end;

begin

definition
let A be Tolerance_Space;
let X, Y be Subset of A;
predX _= Y means :Def14: :: ROUGHS_1:def 14
 LAp X = LAp Y;
reflexivity
 for X being Subset of A holds LAp X = LAp X ;
symmetry
 for X, Y being Subset of A st LAp X = LAp Y holds
LAp Y = LAp X ;
predX =^ Y means :Def15: :: ROUGHS_1:def 15
 UAp X = UAp Y;
reflexivity
 for X being Subset of A holds UAp X = UAp X ;
symmetry
 for X, Y being Subset of A st UAp X = UAp Y holds
UAp Y = UAp X ;
predX _=^ Y means :Def16: :: ROUGHS_1:def 16
( LAp X = LAp Y & UAp X = UAp Y );
reflexivity
 for X being Subset of A holds
( LAp X = LAp X & UAp X = UAp X ) ;
symmetry
 for X, Y being Subset of A st LAp X = LAp Y & UAp X = UAp Y holds
( LAp Y = LAp X & UAp Y = UAp X ) ;
end;

:: deftheorem Def14 defines _= ROUGHS_1:def_14_:_
 for A being Tolerance_Space
for X, Y being Subset of A holds
( X _= Y iff LAp X = LAp Y );

:: deftheorem Def15 defines =^ ROUGHS_1:def_15_:_
 for A being Tolerance_Space
for X, Y being Subset of A holds
( X =^ Y iff UAp X = UAp Y );

:: deftheorem Def16 defines _=^ ROUGHS_1:def_16_:_
 for A being Tolerance_Space
for X, Y being Subset of A holds
( X _=^ Y iff ( LAp X = LAp Y & UAp X = UAp Y ) );

definition
let A be Tolerance_Space;
let X, Y be Subset of A;
redefine pred X _= Y means :: ROUGHS_1:def 17
( X _c= Y & Y _c= X );
compatibility
 ( X _= Y iff ( X _c= Y & Y _c= X ) )
proof
hereby  ::_thesis: ( X _c= Y & Y _c= X implies X _= Y )
assume  X _= Y ; ::_thesis: ( X _c= Y & Y _c= X )
then  LAp X = LAp Y by Def14;
hence  ( X _c= Y & Y _c= X ) by Def11; ::_thesis: verum
end;
assume  ( X _c= Y & Y _c= X ) ; ::_thesis: X _= Y
then  ( LAp X c= LAp Y & LAp Y c= LAp X ) by Def11;
then  LAp X = LAp Y by XBOOLE_0:def_10;
hence  X _= Y by Def14; ::_thesis: verum
end;
redefine pred X =^ Y means :: ROUGHS_1:def 18
( X c=^ Y & Y c=^ X );
compatibility
 ( X =^ Y iff ( X c=^ Y & Y c=^ X ) )
proof
hereby  ::_thesis: ( X c=^ Y & Y c=^ X implies X =^ Y )
assume  X =^ Y ; ::_thesis: ( X c=^ Y & Y c=^ X )
then  UAp X = UAp Y by Def15;
hence  ( X c=^ Y & Y c=^ X ) by Def12; ::_thesis: verum
end;
assume  ( X c=^ Y & Y c=^ X ) ; ::_thesis: X =^ Y
then  ( UAp X c= UAp Y & UAp Y c= UAp X ) by Def12;
then  UAp X = UAp Y by XBOOLE_0:def_10;
hence  X =^ Y by Def15; ::_thesis: verum
end;
redefine pred X _=^ Y means :: ROUGHS_1:def 19
( X _= Y & X =^ Y );
compatibility
 ( X _=^ Y iff ( X _= Y & X =^ Y ) )
proof
hereby  ::_thesis: ( X _= Y & X =^ Y implies X _=^ Y )
assume  X _=^ Y ; ::_thesis: ( X _= Y & X =^ Y )
then  ( LAp X = LAp Y & UAp X = UAp Y ) by Def16;
hence  ( X _= Y & X =^ Y ) by Def14, Def15; ::_thesis: verum
end;
assume  ( X _= Y & X =^ Y ) ; ::_thesis: X _=^ Y
then  ( LAp X = LAp Y & UAp X = UAp Y ) by Def14, Def15;
hence  X _=^ Y by Def16; ::_thesis: verum
end;
end;

:: deftheorem  defines _= ROUGHS_1:def_17_:_
 for A being Tolerance_Space
for X, Y being Subset of A holds
( X _= Y iff ( X _c= Y & Y _c= X ) );

:: deftheorem  defines =^ ROUGHS_1:def_18_:_
 for A being Tolerance_Space
for X, Y being Subset of A holds
( X =^ Y iff ( X c=^ Y & Y c=^ X ) );

:: deftheorem  defines _=^ ROUGHS_1:def_19_:_
 for A being Tolerance_Space
for X, Y being Subset of A holds
( X _=^ Y iff ( X _= Y & X =^ Y ) );