:: On the Lattice of Intervals and Rough Sets
:: by Adam Grabowski and Magdalena Jastrz\c{e}bska
::
:: Received October 10, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

definition
let U be set ;
let X, Y be Subset of U;
func Inter (X,Y) ->  Subset-Family of U equals :: INTERVA1:def 1
 {  A where A is Subset of U : ( X c= A & A c= Y )  }  ;
coherence
  {  A where A is Subset of U : ( X c= A & A c= Y )  }  is Subset-Family of U
proofend;
end;

:: deftheorem  defines Inter INTERVA1:def_1_:_
 for U being set
for X, Y being Subset of U holds Inter (X,Y) =  {  A where A is Subset of U : ( X c= A & A c= Y )  }  ;

theorem Th1: :: INTERVA1:1
for U being set
for X, Y being Subset of U
for x being set holds
( x in Inter (X,Y) iff ( X c= x & x c= Y ) )
proofend;

theorem Th2: :: INTERVA1:2
for U being set
for X, Y being Subset of U st Inter (X,Y) <> {} holds
( X in Inter (X,Y) &amp; Y in Inter (X,Y) )
proofend;

theorem Th3: :: INTERVA1:3
for U being set
for A, B being Subset of U st not A c= B holds
Inter (A,B) = {}
proofend;

theorem :: INTERVA1:4
for U being set
for A, B being Subset of U st Inter (A,B) = {} holds
not A c= B by Th1;

theorem Th5: :: INTERVA1:5
for U being set
for A, B being Subset of U st Inter (A,B) <> {} holds
A c= B
proofend;

theorem Th6: :: INTERVA1:6
for U being set
for A, B, C, D being Subset of U st Inter (A,B) <> {} &amp; Inter (A,B) = Inter (C,D) holds
( A = C &amp; B = D )
proofend;

theorem Th7: :: INTERVA1:7
for U being non empty set
for A being non empty Subset of U holds Inter (A,({} U)) = {}
proofend;

theorem Th8: :: INTERVA1:8
for U being set
for A being Subset of U holds Inter (A,A) = {A}
proofend;

definition
let U be set ;
mode IntervalSet of U ->  Subset-Family of U means :Def2: :: INTERVA1:def 2
 ex A, B being Subset of U st it = Inter (A,B);
existence
 ex b1 being Subset-Family of U ex A, B being Subset of U st b1 = Inter (A,B)
proofend;
end;

:: deftheorem Def2 defines IntervalSet INTERVA1:def_2_:_
 for U being set
for b2 being Subset-Family of U holds
( b2 is IntervalSet of U iff ex A, B being Subset of U st b2 = Inter (A,B) );

theorem :: INTERVA1:9
for U being non empty set holds {} is IntervalSet of U
proofend;

theorem Th10: :: INTERVA1:10
for U being non empty set
for A being Subset of U holds {A} is IntervalSet of U
proofend;

definition
let U be set ;
let A, B be Subset of U;
:: original:Inter
redefine func Inter (A,B) ->  IntervalSet of U;
correctness
coherence
Inter (A,B) is IntervalSet of U;
by Def2;
end;

registration
let U be non empty set ;
cluster non empty for IntervalSet of U;
existence
 not for b1 being IntervalSet of U holds b1 is empty
proofend;
end;

theorem Th11: :: INTERVA1:11
for U being non empty set
for A being set holds
( A is non empty IntervalSet of U iff ex A1, A2 being Subset of U st
( A1 c= A2 &amp; A = Inter (A1,A2) ) )
proofend;

theorem Th12: :: INTERVA1:12
for U being non empty set
for A1, A2, B1, B2 being Subset of U st A1 c= A2 &amp; B1 c= B2 holds
INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) =  {  C where C is Subset of U : ( A1 /\ B1 c= C &amp; C c= A2 /\ B2 )  }
proofend;

theorem Th13: :: INTERVA1:13
for U being non empty set
for A1, A2, B1, B2 being Subset of U st A1 c= A2 &amp; B1 c= B2 holds
UNION ((Inter (A1,A2)),(Inter (B1,B2))) =  {  C where C is Subset of U : ( A1 \/ B1 c= C &amp; C c= A2 \/ B2 )  }
proofend;

definition
let U be non empty set ;
let A, B be non empty IntervalSet of U;
funcA _/\_ B ->  IntervalSet of U equals :: INTERVA1:def 3
 INTERSECTION (A,B);
coherence
 INTERSECTION (A,B) is IntervalSet of U
proofend;
funcA _\/_ B ->  IntervalSet of U equals :: INTERVA1:def 4
 UNION (A,B);
coherence
 UNION (A,B) is IntervalSet of U
proofend;
end;

:: deftheorem  defines _/\_ INTERVA1:def_3_:_
 for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ B = INTERSECTION (A,B);

:: deftheorem  defines _\/_ INTERVA1:def_4_:_
 for U being non empty set
for A, B being non empty IntervalSet of U holds A _\/_ B = UNION (A,B);

registration
let U be non empty set ;
let A, B be non empty IntervalSet of U;
clusterA _/\_ B ->  non empty ;
coherence
 not A _/\_ B is empty by TOPGEN_4:31;
clusterA _\/_ B ->  non empty ;
coherence
 not A _\/_ B is empty by TOPGEN_4:30;
end;

definition
let U be non empty set ;
let A be non empty IntervalSet of U;
funcA ``1  ->  Subset of U means :Def5: :: INTERVA1:def 5
 ex B being Subset of U st A = Inter (it,B);
existence
 ex b1, B being Subset of U st A = Inter (b1,B)
proofend;
uniqueness
 for b1, b2 being Subset of U st ex B being Subset of U st A = Inter (b1,B) &amp; ex B being Subset of U st A = Inter (b2,B) holds
b1 = b2 by Th6;
funcA ``2  ->  Subset of U means :Def6: :: INTERVA1:def 6
 ex B being Subset of U st A = Inter (B,it);
existence
 ex b1, B being Subset of U st A = Inter (B,b1)
proofend;
uniqueness
 for b1, b2 being Subset of U st ex B being Subset of U st A = Inter (B,b1) &amp; ex B being Subset of U st A = Inter (B,b2) holds
b1 = b2 by Th6;
end;

:: deftheorem Def5 defines ``1 INTERVA1:def_5_:_
 for U being non empty set
for A being non empty IntervalSet of U
for b3 being Subset of U holds
( b3 = A ``1 iff ex B being Subset of U st A = Inter (b3,B) );

:: deftheorem Def6 defines ``2 INTERVA1:def_6_:_
 for U being non empty set
for A being non empty IntervalSet of U
for b3 being Subset of U holds
( b3 = A ``2 iff ex B being Subset of U st A = Inter (B,b3) );

theorem Th14: :: INTERVA1:14
for U being non empty set
for A being non empty IntervalSet of U
for X being set holds
( X in A iff ( A ``1 c= X &amp; X c= A ``2 ) )
proofend;

theorem Th15: :: INTERVA1:15
for U being non empty set
for A being non empty IntervalSet of U holds A = Inter ((A ``1),(A ``2))
proofend;

theorem Th16: :: INTERVA1:16
for U being non empty set
for A being non empty IntervalSet of U holds A ``1 c= A ``2
proofend;

theorem Th17: :: INTERVA1:17
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\/_ B = Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2)))
proofend;

theorem Th18: :: INTERVA1:18
for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ B = Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2)))
proofend;

definition
let U be non empty set ;
let A, B be non empty IntervalSet of U;
:: original:=
redefine predA = B means :: INTERVA1:def 7
( A ``1 = B ``1 &amp; A ``2 = B ``2 );
compatibility
 ( A = B iff ( A ``1 = B ``1 &amp; A ``2 = B ``2 ) )
proofend;
end;

:: deftheorem  defines = INTERVA1:def_7_:_
 for U being non empty set
for A, B being non empty IntervalSet of U holds
( A = B iff ( A ``1 = B ``1 &amp; A ``2 = B ``2 ) );

theorem :: INTERVA1:19
for U being non empty set
for A being non empty IntervalSet of U holds A _\/_ A = A
proofend;

theorem :: INTERVA1:20
for U being non empty set
for A being non empty IntervalSet of U holds A _/\_ A = A
proofend;

theorem :: INTERVA1:21
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\/_ B = B _\/_ A ;

theorem :: INTERVA1:22
for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ B = B _/\_ A ;

theorem Th23: :: INTERVA1:23
for U being non empty set
for A, B, C being non empty IntervalSet of U holds (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)
proofend;

theorem Th24: :: INTERVA1:24
for U being non empty set
for A, B, C being non empty IntervalSet of U holds (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
proofend;

Lm1:  for X being set
for A, B, C being Subset-Family of X holds UNION (A,(INTERSECTION (B,C))) c= INTERSECTION ((UNION (A,B)),(UNION (A,C)))
proofend;

definition
let X be set ;
let F be Subset-Family of X;
attrF is ordered  means :Def8: :: INTERVA1:def 8
 ex A, B being set st
( A in F &amp; B in F &amp; ( for Y being set holds
( Y in F iff ( A c= Y &amp; Y c= B ) ) ) );
end;

:: deftheorem Def8 defines ordered INTERVA1:def_8_:_
 for X being set
for F being Subset-Family of X holds
( F is ordered iff ex A, B being set st
( A in F &amp; B in F &amp; ( for Y being set holds
( Y in F iff ( A c= Y &amp; Y c= B ) ) ) ) );

registration
let X be set ;
cluster non empty ordered for Element of K19(K19(X));
existence
 ex b1 being Subset-Family of X st
( not b1 is empty &amp; b1 is ordered )
proofend;
end;

theorem Th25: :: INTERVA1:25
for U being non empty set
for A, B being Subset of U st A c= B holds
Inter (A,B) is non empty ordered Subset-Family of U
proofend;

theorem Th26: :: INTERVA1:26
for U being non empty set
for A being non empty IntervalSet of U holds A is non empty ordered Subset-Family of U
proofend;

notation
let X be set ;
synonym  min X for  meet X;
synonym  max X for  union X;
end;

definition
let X be set ;
let F be non empty ordered Subset-Family of X;
:: original:min
redefine func min F ->  Element of F;
correctness
coherence
min F is Element of F;
proofend;
:: original:max
redefine func max F ->  Element of F;
correctness
coherence
max F is Element of F;
proofend;
end;

Lm2:  for X being set
for F being non empty ordered Subset-Family of X
for G being set st G in F holds
( G = min F iff for Y being set st Y in F holds
G c= Y )
proofend;

Lm3:  for X being set
for F being non empty ordered Subset-Family of X
for G being set st G in F holds
( G = max F iff for Y being set st Y in F holds
Y c= G )
proofend;

theorem Th27: :: INTERVA1:27
for U being non empty set
for A, B being Subset of U
for F being non empty ordered Subset-Family of U st F = Inter (A,B) holds
( min F = A &amp; max F = B )
proofend;

theorem Th28: :: INTERVA1:28
for X, Y being set
for A being non empty ordered Subset-Family of X holds
( Y in A iff ( min A c= Y &amp; Y c= max A ) )
proofend;

Lm4:  for U being non empty set
for A being non empty IntervalSet of U holds A is non empty ordered Subset-Family of U
by Th26;

theorem Th29: :: INTERVA1:29
for X being set
for A, B, C being non empty ordered Subset-Family of X holds UNION (A,(INTERSECTION (B,C))) = INTERSECTION ((UNION (A,B)),(UNION (A,C)))
proofend;

Lm5:  for X being set
for A, B, C being Subset-Family of X holds INTERSECTION (A,(UNION (B,C))) c= UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
proofend;

theorem Th30: :: INTERVA1:30
for X being set
for A, B, C being non empty ordered Subset-Family of X holds INTERSECTION (A,(UNION (B,C))) = UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
proofend;

theorem :: INTERVA1:31
for U being non empty set
for A, B, C being non empty IntervalSet of U holds A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C)
proofend;

theorem :: INTERVA1:32
for U being non empty set
for A, B, C being non empty IntervalSet of U holds A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
proofend;

theorem Th33: :: INTERVA1:33
for X being set
for A, B being non empty ordered Subset-Family of X holds INTERSECTION (A,(UNION (A,B))) = A
proofend;

theorem Th34: :: INTERVA1:34
for X being set
for A, B being non empty ordered Subset-Family of X holds UNION ((INTERSECTION (A,B)),B) = B
proofend;

theorem Th35: :: INTERVA1:35
for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ (A _\/_ B) = A
proofend;

theorem Th36: :: INTERVA1:36
for U being non empty set
for A, B being non empty IntervalSet of U holds (A _/\_ B) _\/_ B = B
proofend;

begin

theorem Th37: :: INTERVA1:37
for U being non empty set
for A, B being Subset-Family of U holds DIFFERENCE (A,B) is Subset-Family of U
proofend;

theorem Th38: :: INTERVA1:38
for U being non empty set
for A, B being non empty ordered Subset-Family of U holds DIFFERENCE (A,B) =  {  C where C is Subset of U : ( (min A) \ (max B) c= C &amp; C c= (max A) \ (min B) )  }
proofend;

theorem Th39: :: INTERVA1:39
for U being non empty set
for A1, A2, B1, B2 being Subset of U st A1 c= A2 &amp; B1 c= B2 holds
DIFFERENCE ((Inter (A1,A2)),(Inter (B1,B2))) =  {  C where C is Subset of U : ( A1 \ B2 c= C &amp; C c= A2 \ B1 )  }
proofend;

definition
let U be non empty set ;
let A, B be non empty IntervalSet of U;
funcA _\_ B ->  IntervalSet of U equals :: INTERVA1:def 9
 DIFFERENCE (A,B);
coherence
 DIFFERENCE (A,B) is IntervalSet of U
proofend;
end;

:: deftheorem  defines _\_ INTERVA1:def_9_:_
 for U being non empty set
for A, B being non empty IntervalSet of U holds A _\_ B = DIFFERENCE (A,B);

registration
let U be non empty set ;
let A, B be non empty IntervalSet of U;
clusterA _\_ B ->  non empty ;
coherence
 not A _\_ B is empty
proofend;
end;

theorem Th40: :: INTERVA1:40
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\_ B = Inter (((A ``1) \ (B ``2)),((A ``2) \ (B ``1)))
proofend;

theorem Th41: :: INTERVA1:41
for U being non empty set
for A, C being non empty IntervalSet of U
for X, Y being Subset of U st A = Inter (X,Y) holds
A _\_ C = Inter ((X \ (C ``2)),(Y \ (C ``1)))
proofend;

theorem Th42: :: INTERVA1:42
for U being non empty set
for A, C being non empty IntervalSet of U
for X, Y, W, Z being Subset of U st A = Inter (X,Y) &amp; C = Inter (W,Z) holds
A _\_ C = Inter ((X \ Z),(Y \ W))
proofend;

theorem Th43: :: INTERVA1:43
for U being non empty set holds Inter (([#] U),([#] U)) is non empty IntervalSet of U
proofend;

theorem Th44: :: INTERVA1:44
for U being non empty set holds Inter (({} U),({} U)) is non empty IntervalSet of U
proofend;

registration
let U be non empty set ;
cluster Inter (([#] U),([#] U)) ->  non empty ;
coherence
 not Inter (([#] U),([#] U)) is empty by Th43;
cluster Inter (({} U),({} U)) ->  non empty ;
coherence
 not Inter (({} U),({} U)) is empty by Th44;
end;

definition
let U be non empty set ;
let A be non empty IntervalSet of U;
funcA ^  ->  non empty IntervalSet of U equals :: INTERVA1:def 10
(Inter (([#] U),([#] U))) _\_ A;
coherence
 (Inter (([#] U),([#] U))) _\_ A is non empty IntervalSet of U ;
end;

:: deftheorem  defines ^ INTERVA1:def_10_:_
 for U being non empty set
for A being non empty IntervalSet of U holds A ^ = (Inter (([#] U),([#] U))) _\_ A;

theorem Th45: :: INTERVA1:45
for U being non empty set
for A being non empty IntervalSet of U holds A ^ = Inter (((A ``2) `),((A ``1) `)) by Th41;

theorem Th46: :: INTERVA1:46
for U being non empty set
for A being non empty IntervalSet of U
for X, Y being Subset of U st A = Inter (X,Y) &amp; X c= Y holds
A ^ = Inter ((Y `),(X `))
proofend;

theorem :: INTERVA1:47
for U being non empty set holds (Inter (({} U),({} U))) ^ = Inter (([#] U),([#] U))
proofend;

theorem :: INTERVA1:48
for U being non empty set holds (Inter (([#] U),([#] U))) ^ = Inter (({} U),({} U))
proofend;

begin

theorem :: INTERVA1:49
for U being non empty set ex A being non empty IntervalSet of U st (A _/\_ A) ^ <> Inter (({} U),({} U))
proofend;

theorem :: INTERVA1:50
for U being non empty set ex A being non empty IntervalSet of U st (A _\/_ A) ^ <> Inter (([#] U),([#] U))
proofend;

theorem :: INTERVA1:51
for U being non empty set ex A being non empty IntervalSet of U st A _\_ A <> Inter (({} U),({} U))
proofend;

theorem :: INTERVA1:52
for U being non empty set
for A being non empty IntervalSet of U holds U in A _\/_ (A ^)
proofend;

theorem :: INTERVA1:53
for U being non empty set
for A being non empty IntervalSet of U holds {} in A _/\_ (A ^)
proofend;

theorem :: INTERVA1:54
for U being non empty set
for A being non empty IntervalSet of U holds {} in A _\_ A
proofend;

begin

definition
let U be non empty set ;
func IntervalSets U ->  non empty set  means :Def11: :: INTERVA1:def 11
 for x being set holds
( x in it iff x is non empty IntervalSet of U );
existence
 ex b1 being non empty set st
for x being set holds
( x in b1 iff x is non empty IntervalSet of U )
proofend;
uniqueness
 for b1, b2 being non empty set st ( for x being set holds
( x in b1 iff x is non empty IntervalSet of U ) ) &amp; ( for x being set holds
( x in b2 iff x is non empty IntervalSet of U ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines IntervalSets INTERVA1:def_11_:_
 for U, b2 being non empty set holds
( b2 = IntervalSets U iff for x being set holds
( x in b2 iff x is non empty IntervalSet of U ) );

definition
let U be non empty set ;
func InterLatt U ->  non empty strict LattStr  means :Def12: :: INTERVA1:def 12
( the carrier of it = IntervalSets U &amp; ( for a, b being Element of the carrier of it
for a9, b9 being non empty IntervalSet of U st a9 = a &amp; b9 = b holds
( the L_join of it . (a,b) = a9 _\/_ b9 &amp; the L_meet of it . (a,b) = a9 _/\_ b9 ) ) );
existence
 ex b1 being non empty strict LattStr st
( the carrier of b1 = IntervalSets U &amp; ( for a, b being Element of the carrier of b1
for a9, b9 being non empty IntervalSet of U st a9 = a &amp; b9 = b holds
( the L_join of b1 . (a,b) = a9 _\/_ b9 &amp; the L_meet of b1 . (a,b) = a9 _/\_ b9 ) ) )
proofend;
uniqueness
 for b1, b2 being non empty strict LattStr st the carrier of b1 = IntervalSets U &amp; ( for a, b being Element of the carrier of b1
for a9, b9 being non empty IntervalSet of U st a9 = a &amp; b9 = b holds
( the L_join of b1 . (a,b) = a9 _\/_ b9 &amp; the L_meet of b1 . (a,b) = a9 _/\_ b9 ) ) &amp; the carrier of b2 = IntervalSets U &amp; ( for a, b being Element of the carrier of b2
for a9, b9 being non empty IntervalSet of U st a9 = a &amp; b9 = b holds
( the L_join of b2 . (a,b) = a9 _\/_ b9 &amp; the L_meet of b2 . (a,b) = a9 _/\_ b9 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines InterLatt INTERVA1:def_12_:_
 for U being non empty set
for b2 being non empty strict LattStr holds
( b2 = InterLatt U iff ( the carrier of b2 = IntervalSets U &amp; ( for a, b being Element of the carrier of b2
for a9, b9 being non empty IntervalSet of U st a9 = a &amp; b9 = b holds
( the L_join of b2 . (a,b) = a9 _\/_ b9 &amp; the L_meet of b2 . (a,b) = a9 _/\_ b9 ) ) ) );

registration
let U be non empty set ;
cluster InterLatt U ->  non empty strict Lattice-like ;
correctness
coherence
InterLatt U is Lattice-like ;
proofend;
end;

definition
let X be Tolerance_Space;
mode RoughSet of X ->  Element of [:(bool the carrier of X),(bool the carrier of X):] means :Def13: :: INTERVA1:def 13
verum;
existence
 ex b1 being Element of [:(bool the carrier of X),(bool the carrier of X):] st verum ;
end;

:: deftheorem Def13 defines RoughSet INTERVA1:def_13_:_
 for X being Tolerance_Space
for b2 being Element of [:(bool the carrier of X),(bool the carrier of X):] holds
( b2 is RoughSet of X iff verum );

theorem Th55: :: INTERVA1:55
for X being Tolerance_Space
for A being RoughSet of X ex B, C being Subset of X st A = [B,C]
proofend;

definition
let X be Tolerance_Space;
let A be Subset of X;
func RS A ->  RoughSet of X equals :: INTERVA1:def 14
[(LAp A),(UAp A)];
coherence
 [(LAp A),(UAp A)] is RoughSet of X
proofend;
end;

:: deftheorem  defines RS INTERVA1:def_14_:_
 for X being Tolerance_Space
for A being Subset of X holds RS A = [(LAp A),(UAp A)];

definition
let X be Tolerance_Space;
let A be RoughSet of X;
func LAp A ->  Subset of X equals :: INTERVA1:def 15
A `1 ;
coherence
 A `1 is Subset of X
proofend;
func UAp A ->  Subset of X equals :: INTERVA1:def 16
A `2 ;
coherence
 A `2 is Subset of X
proofend;
end;

:: deftheorem  defines LAp INTERVA1:def_15_:_
 for X being Tolerance_Space
for A being RoughSet of X holds LAp A = A `1 ;

:: deftheorem  defines UAp INTERVA1:def_16_:_
 for X being Tolerance_Space
for A being RoughSet of X holds UAp A = A `2 ;

definition
let X be Tolerance_Space;
let A, B be RoughSet of X;
:: original:=
redefine predA = B means :Def17: :: INTERVA1:def 17
( LAp A = LAp B &amp; UAp A = UAp B );
compatibility
 ( A = B iff ( LAp A = LAp B &amp; UAp A = UAp B ) )
proofend;
end;

:: deftheorem Def17 defines = INTERVA1:def_17_:_
 for X being Tolerance_Space
for A, B being RoughSet of X holds
( A = B iff ( LAp A = LAp B &amp; UAp A = UAp B ) );

definition
let X be Tolerance_Space;
let A, B be RoughSet of X;
funcA _\/_ B ->  RoughSet of X equals :: INTERVA1:def 18
[((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))];
coherence
 [((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))] is RoughSet of X
proofend;
funcA _/\_ B ->  RoughSet of X equals :: INTERVA1:def 19
[((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))];
coherence
 [((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))] is RoughSet of X
proofend;
end;

:: deftheorem  defines _\/_ INTERVA1:def_18_:_
 for X being Tolerance_Space
for A, B being RoughSet of X holds A _\/_ B = [((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))];

:: deftheorem  defines _/\_ INTERVA1:def_19_:_
 for X being Tolerance_Space
for A, B being RoughSet of X holds A _/\_ B = [((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))];

theorem Th56: :: INTERVA1:56
for X being Tolerance_Space
for A, B being RoughSet of X holds LAp (A _\/_ B) = (LAp A) \/ (LAp B) by MCART_1:7;

theorem Th57: :: INTERVA1:57
for X being Tolerance_Space
for A, B being RoughSet of X holds UAp (A _\/_ B) = (UAp A) \/ (UAp B) by MCART_1:7;

theorem Th58: :: INTERVA1:58
for X being Tolerance_Space
for A, B being RoughSet of X holds LAp (A _/\_ B) = (LAp A) /\ (LAp B) by MCART_1:7;

theorem Th59: :: INTERVA1:59
for X being Tolerance_Space
for A, B being RoughSet of X holds UAp (A _/\_ B) = (UAp A) /\ (UAp B) by MCART_1:7;

:: Properties
theorem :: INTERVA1:60
for X being Tolerance_Space
for A being RoughSet of X holds A _\/_ A = A
proofend;

theorem Th61: :: INTERVA1:61
for X being Tolerance_Space
for A being RoughSet of X holds A _/\_ A = A
proofend;

theorem :: INTERVA1:62
for X being Tolerance_Space
for A, B being RoughSet of X holds A _\/_ B = B _\/_ A ;

theorem :: INTERVA1:63
for X being Tolerance_Space
for A, B being RoughSet of X holds A _/\_ B = B _/\_ A ;

theorem Th64: :: INTERVA1:64
for X being Tolerance_Space
for A, B, C being RoughSet of X holds (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)
proofend;

theorem Th65: :: INTERVA1:65
for X being Tolerance_Space
for A, B, C being RoughSet of X holds (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
proofend;

theorem Th66: :: INTERVA1:66
for X being Tolerance_Space
for A, B, C being RoughSet of X holds A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
proofend;

theorem Th67: :: INTERVA1:67
for X being Tolerance_Space
for A, B being RoughSet of X holds A _\/_ (A _/\_ B) = A
proofend;

theorem :: INTERVA1:68
for X being Tolerance_Space
for A, B being RoughSet of X holds A _/\_ (A _\/_ B) = A
proofend;

begin

definition
let X be Tolerance_Space;
func RoughSets X ->  set  means :Def20: :: INTERVA1:def 20
 for x being set holds
( x in it iff x is RoughSet of X );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is RoughSet of X )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is RoughSet of X ) ) &amp; ( for x being set holds
( x in b2 iff x is RoughSet of X ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def20 defines RoughSets INTERVA1:def_20_:_
 for X being Tolerance_Space
for b2 being set holds
( b2 = RoughSets X iff for x being set holds
( x in b2 iff x is RoughSet of X ) );

registration
let X be Tolerance_Space;
cluster RoughSets X ->  non empty ;
coherence
 not RoughSets X is empty
proofend;
end;

definition
let X be Tolerance_Space;
let R be Element of RoughSets X;
func @ R ->  RoughSet of X equals :: INTERVA1:def 21
R;
coherence
 R is RoughSet of X by Def20;
end;

:: deftheorem  defines @ INTERVA1:def_21_:_
 for X being Tolerance_Space
for R being Element of RoughSets X holds @ R = R;

definition
let X be Tolerance_Space;
let R be RoughSet of X;
funcR @  ->  Element of RoughSets X equals :: INTERVA1:def 22
R;
coherence
 R is Element of RoughSets X by Def20;
end;

:: deftheorem  defines @ INTERVA1:def_22_:_
 for X being Tolerance_Space
for R being RoughSet of X holds R @ = R;

definition
let X be Tolerance_Space;
func RSLattice X ->  strict LattStr  means :Def23: :: INTERVA1:def 23
( the carrier of it = RoughSets X &amp; ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 &amp; B = B9 holds
( the L_join of it . (A,B) = A9 _\/_ B9 &amp; the L_meet of it . (A,B) = A9 _/\_ B9 ) ) );
existence
 ex b1 being strict LattStr st
( the carrier of b1 = RoughSets X &amp; ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 &amp; B = B9 holds
( the L_join of b1 . (A,B) = A9 _\/_ B9 &amp; the L_meet of b1 . (A,B) = A9 _/\_ B9 ) ) )
proofend;
uniqueness
 for b1, b2 being strict LattStr st the carrier of b1 = RoughSets X &amp; ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 &amp; B = B9 holds
( the L_join of b1 . (A,B) = A9 _\/_ B9 &amp; the L_meet of b1 . (A,B) = A9 _/\_ B9 ) ) &amp; the carrier of b2 = RoughSets X &amp; ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 &amp; B = B9 holds
( the L_join of b2 . (A,B) = A9 _\/_ B9 &amp; the L_meet of b2 . (A,B) = A9 _/\_ B9 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def23 defines RSLattice INTERVA1:def_23_:_
 for X being Tolerance_Space
for b2 being strict LattStr holds
( b2 = RSLattice X iff ( the carrier of b2 = RoughSets X &amp; ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 &amp; B = B9 holds
( the L_join of b2 . (A,B) = A9 _\/_ B9 &amp; the L_meet of b2 . (A,B) = A9 _/\_ B9 ) ) ) );

registration
let X be Tolerance_Space;
cluster RSLattice X ->  non empty strict ;
coherence
 not RSLattice X is empty
proofend;
end;

Lm6:  for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "\/" b = b "\/" a
proofend;

Lm7:  for X being Tolerance_Space
for a, b, c being Element of (RSLattice X) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proofend;

Lm8:  for X being Tolerance_Space
for K, L being Element of RoughSets X holds the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),L) = L
proofend;

Lm9:  for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds (a "/\" b) "\/" b = b
proofend;

Lm10:  for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "/\" b = b "/\" a
proofend;

Lm11:  for X being Tolerance_Space
for a, b, c being Element of (RSLattice X) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proofend;

Lm12:  for X being Tolerance_Space
for K, L, M being Element of RoughSets X holds the L_meet of (RSLattice X) . (K,( the L_join of (RSLattice X) . (L,M))) = the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),( the L_meet of (RSLattice X) . (K,M)))
proofend;

Lm13:  for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "/\" (a "\/" b) = a
proofend;

registration
let X be Tolerance_Space;
cluster RSLattice X ->  strict Lattice-like ;
coherence
 RSLattice X is Lattice-like
proofend;
end;

registration
let X be Tolerance_Space;
cluster RSLattice X ->  strict distributive ;
coherence
 RSLattice X is distributive
proofend;
end;

definition
let X be Tolerance_Space;
func ERS X ->  RoughSet of X equals :: INTERVA1:def 24
[{},{}];
coherence
 [{},{}] is RoughSet of X
proofend;
end;

:: deftheorem  defines ERS INTERVA1:def_24_:_
 for X being Tolerance_Space holds ERS X = [{},{}];

Lm14:  for X being Tolerance_Space holds ERS X in RoughSets X
by Def20;

theorem Th69: :: INTERVA1:69
for X being Tolerance_Space
for A being RoughSet of X holds (ERS X) _\/_ A = A
proofend;

definition
let X be Tolerance_Space;
func TRS X ->  RoughSet of X equals :: INTERVA1:def 25
[([#] X),([#] X)];
coherence
 [([#] X),([#] X)] is RoughSet of X
proofend;
end;

:: deftheorem  defines TRS INTERVA1:def_25_:_
 for X being Tolerance_Space holds TRS X = [([#] X),([#] X)];

Lm15:  for X being Tolerance_Space holds TRS X in RoughSets X
by Def20;

theorem Th70: :: INTERVA1:70
for X being Tolerance_Space
for A being RoughSet of X holds (TRS X) _/\_ A = A
proofend;

registration
let X be Tolerance_Space;
cluster RSLattice X ->  strict bounded ;
coherence
 RSLattice X is bounded
proofend;
end;

theorem Th71: :: INTERVA1:71
for X being Tolerance_Space
for A, B being Element of (RSLattice X)
for A9, B9 being RoughSet of X st A = A9 &amp; B = B9 holds
( A [= B iff ( LAp A9 c= LAp B9 &amp; UAp A9 c= UAp B9 ) )
proofend;

Lm16:  for X being Tolerance_Space holds RSLattice X is complete
proofend;

registration
let X be Tolerance_Space;
cluster RSLattice X ->  strict complete ;
coherence
 RSLattice X is complete by Lm16;
end;