:: Basic Properties of Rough Sets and Rough Membership Function
:: by Adam Grabowski
::
:: Received November 23, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


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
proofend;

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
proofend;
end;

theorem :: ROUGHS_1:2
for L being reflexive RelStr holds id the carrier of L c= the InternalRel of L
proofend;

Lm1:  for A being RelStr st A is reflexive & A is trivial holds
A is discrete
proofend;

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
proofend;

Lm2:  for A being RelStr st A is discrete holds
A is diagonal
proofend;

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 )
proofend;
end;

theorem Th4: :: ROUGHS_1:4
for A being non empty non diagonal RelStr ex x, y being Element of A st
( x <> y &amp; [x,y] in the InternalRel of A )
proofend;

theorem Th5: :: ROUGHS_1:5
for D being set
for p, q being FinSequence of D holds Union (p ^ q) = (Union p) \/ (Union q)
proofend;

theorem Th6: :: ROUGHS_1:6
for p, q being Function st q is disjoint_valued &amp; p c= q holds
p is disjoint_valued
proofend;

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
proofend;
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
proofend;
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 &amp; b1 is disjoint_valued )
proofend;
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
proofend;
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
proofend;
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)
proofend;

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
proofend;
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 &amp; b1 is finite &amp; b1 is with_equivalence &amp; not b1 is empty )
proofend;
cluster non empty finite non diagonal with_equivalence for RelStr ;
existence
 ex b1 being RelStr st
( not b1 is diagonal &amp; b1 is finite &amp; b1 is with_equivalence &amp; not b1 is empty )
proofend;
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 &amp; the InternalRel of A is reflexive &amp; 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
proofend;
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
proofend;
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
proofend;

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
proofend;

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
proofend;

theorem Th13: :: ROUGHS_1:13
for A being Tolerance_Space
for X being Subset of A holds X c= UAp X
proofend;

theorem Th14: :: ROUGHS_1:14
for A being Tolerance_Space
for X being Subset of A holds LAp X c= UAp X
proofend;

theorem Th15: :: ROUGHS_1:15
for A being Tolerance_Space
for X being Subset of A holds
( X is exact iff LAp X = X )
proofend;

theorem Th16: :: ROUGHS_1:16
for A being Tolerance_Space
for X being Subset of A holds
( X is exact iff UAp X = X )
proofend;

theorem :: ROUGHS_1:17
for A being Tolerance_Space
for X being Subset of A holds
( X = LAp X iff X = UAp X )
proofend;

theorem Th18: :: ROUGHS_1:18
for A being Tolerance_Space holds LAp ({} A) = {}
proofend;

theorem Th19: :: ROUGHS_1:19
for A being Tolerance_Space holds UAp ({} A) = {}
proofend;

theorem Th20: :: ROUGHS_1:20
for A being Tolerance_Space holds LAp ([#] A) = [#] A
proofend;

theorem :: ROUGHS_1:21
for A being Tolerance_Space holds UAp ([#] A) = [#] A
proofend;

theorem :: ROUGHS_1:22
for A being Tolerance_Space
for X, Y being Subset of A holds LAp (X /\ Y) = (LAp X) /\ (LAp Y)
proofend;

theorem :: ROUGHS_1:23
for A being Tolerance_Space
for X, Y being Subset of A holds UAp (X \/ Y) = (UAp X) \/ (UAp Y)
proofend;

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
proofend;

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
proofend;

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)
proofend;

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)
proofend;

theorem Th28: :: ROUGHS_1:28
for A being Tolerance_Space
for X being Subset of A holds LAp (X `) = (UAp X) `
proofend;

theorem Th29: :: ROUGHS_1:29
for A being Tolerance_Space
for X being Subset of A holds UAp (X `) = (LAp X) `
proofend;

theorem :: ROUGHS_1:30
for A being Tolerance_Space
for X being Subset of A holds UAp (LAp (UAp X)) = UAp X
proofend;

theorem :: ROUGHS_1:31
for A being Tolerance_Space
for X being Subset of A holds LAp (UAp (LAp X)) = LAp X
proofend;

theorem :: ROUGHS_1:32
for A being Tolerance_Space
for X being Subset of A holds BndAp X = BndAp (X `)
proofend;

theorem :: ROUGHS_1:33
for A being Approximation_Space
for X being Subset of A holds LAp (LAp X) = LAp X
proofend;

theorem Th34: :: ROUGHS_1:34
for A being Approximation_Space
for X being Subset of A holds LAp (LAp X) = UAp (LAp X)
proofend;

theorem :: ROUGHS_1:35
for A being Approximation_Space
for X being Subset of A holds UAp (UAp X) = UAp X
proofend;

theorem Th36: :: ROUGHS_1:36
for A being Approximation_Space
for X being Subset of A holds UAp (UAp X) = LAp (UAp X)
proofend;

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
proofend;
end;

registration
let A be Approximation_Space;
let X be Subset of A;
cluster LAp X ->  exact ;
coherence
 not LAp X is rough
proofend;
cluster UAp X ->  exact ;
coherence
 not UAp X is rough
proofend;
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 &amp; [x,y] in the InternalRel of A holds
y in UAp X
proofend;

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
proofend;
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
proofend;
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)))
proofend;
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))) ) &amp; ( 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
proofend;
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 &amp; (MemberFunc (X,A)) . x <= 1 )
proofend;

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.]
proofend;

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 )
proofend;

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) ` )
proofend;

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 &amp; (MemberFunc (X,A)) . x < 1 ) iff x in BndAp X )
proofend;

theorem Th43: :: ROUGHS_1:43
for A being discrete Approximation_Space
for X being Subset of A holds X is exact
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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
proofend;

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))
proofend;

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)
proofend;

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))
proofend;

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 &amp; ( 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 &amp; ( for n being Nat st n in dom X holds
b1 . n = (MemberFunc ((X . n),A)) . x ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of REAL st dom b1 = dom X &amp; ( for n being Nat st n in dom X holds
b1 . n = (MemberFunc ((X . n),A)) . x ) &amp; dom b2 = dom X &amp; ( for n being Nat st n in dom X holds
b2 . n = (MemberFunc ((X . n),A)) . x ) holds
b1 = b2
proofend;
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 &amp; ( 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)*>
proofend;

theorem Th54: :: ROUGHS_1:54
for A being finite Approximation_Space
for x being Element of A holds (MemberFunc (({} A),A)) . x = 0
proofend;

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))
proofend;

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  }
proofend;

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  }
proofend;

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 &amp; (MemberFunc (X,A)) . x < 1 )  }
proofend;

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 &amp; X c=^ Y );
reflexivity
 for X being Subset of A holds
( X _c= X &amp; 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 &amp; 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 &amp; Y _c= Z holds
X _c= Z
proofend;

theorem Th60: :: ROUGHS_1:60
for A being Tolerance_Space
for X, Y, Z being Subset of A st X c=^ Y &amp; Y c=^ Z holds
X c=^ Z
proofend;

theorem :: ROUGHS_1:61
for A being Tolerance_Space
for X, Y, Z being Subset of A st X _c=^ Y &amp; Y _c=^ Z holds
X _c=^ Z
proofend;

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 &amp; UAp X = UAp Y );
reflexivity
 for X being Subset of A holds
( LAp X = LAp X &amp; UAp X = UAp X ) ;
symmetry
 for X, Y being Subset of A st LAp X = LAp Y &amp; UAp X = UAp Y holds
( LAp Y = LAp X &amp; 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 &amp; 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 &amp; Y _c= X );
compatibility
 ( X _= Y iff ( X _c= Y &amp; Y _c= X ) )
proofend;
redefine pred X =^ Y means :: ROUGHS_1:def 18
( X c=^ Y &amp; Y c=^ X );
compatibility
 ( X =^ Y iff ( X c=^ Y &amp; Y c=^ X ) )
proofend;
redefine pred X _=^ Y means :: ROUGHS_1:def 19
( X _= Y &amp; X =^ Y );
compatibility
 ( X _=^ Y iff ( X _= Y &amp; X =^ Y ) )
proofend;
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 &amp; 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 &amp; 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 &amp; X =^ Y ) );